(* requires true *) (* returns r where (r = x or r = y) and r >=x and r >= y *) fun max2(x,y) = if y > x then y else x
We derived the vc and argued informally that it was valid.
We started with the code for lmax from a previous lecture:
(* requires lst != nil *) (* returns r where r∈lst and (∀x. x∈lst ⇒ r≥x) *) fun lmax(lst) = case lst of [x] => x | h::t => max2(h, lmax(t))
Then we made it tail recursive:
fun lmaxTr(lst, curMax) = case lst of [x] => max2(x, curMax) | h::t => lmaxTr(t, max2(h, curMax))
To argue that the tail recursive version is correct, we needed a new spec:
(* requires lst != nil *) (* returns r where r is the maximum of curMax and the elements of lst *)
We chose not to write the postcondition in fully formal predicate logic; the English version was good enough for our purposes.
The previous example was easy. But sometimes converting to tail recursion is harder. Consider an algorithm you learned in CS 280:
(* requires n >= 0 *) (* returns x^n *) fun expRs(x,n) = if n = 0 then 1 else if n mod 2 = 0 then (* n is even *) let y = expRs(x, n div 2) in y * y else (* n is odd *) let y = expRs(x, (n-1) div 2) in x * y * y
Why does this work? Because of an identity for exponentiation:
x^{n} = 1 if n = 0 (x^{2})^{n/2}} if n is even x * (x^{2})^^{(n-1)/2} if n is odd
Why would we want to use this algorithm? It requires only O(log n) multiplications, instead of the naive O(n) implementation. To start making this tail recursive, we (as usual) introduce an accumulator, then rewrite the body to use only tail calls:
fun expRsTr(x, n, acc) = if n = 0 then ? else if n mod 2 = 0 then (* n is even *) expRsTr( ?, ?, ? ) else (* n is odd *) expRsTr( ?, ?, ? )
How can we figure out what expressions to fill in for each branch? One very effective way to do this is to write the new spec, then use it to solve for those expressions. We have a lot of freedom in designing the new spec, but let's start with something simple:
(* requires n >= 0 *) (* returns acc * x^n *)
Now we know that each branch needs to return acc * x^{n}. For the first branch, where n = 0, this means that we need to return acc * x^{n}, which is just acc. We now have:
(* requires n >= 0 *) (* returns acc * x^n *) fun expRsTr(x, n, acc) = if n = 0 then acc else if n mod 2 = 0 then (* n is even *) expRsTr( ?, ?, ? ) else (* n is odd *) expRsTr( ?, ?, ? )
For the second branch, where n is even, we also need to return acc * x^{n}.
We get to assume that the recursive call to expRsTr
in this branch will satisfy
its postcondition. So let's assume we fill in expRsTr
(a,b,c); the call would
return c * a^{b}. So we now have an equation: acc * x^{n} =
c * a^{b}. This is an underdetermined equation, so let's use two
heuristics. (1) Fill in a piece we know from expRs: b = n div 2. (2) Simple
pattern matching on the equation suggests c = acc. We now have: acc *
x^{n} = acc * a^{n div 2}. Solving for a (using the identity
from before), we get a = x^{2}. So our code for this branch is:
(* requires n >= 0 *) (* returns acc * x^n *) fun expRsTr(x, n, acc) = if n = 0 then acc else if n mod 2 = 0 then (* n is even *) expRsTr(x*x, n div 2, acc) else (* n is odd *) expRsTr( ?, ?, ? )
Repeating the same process for the third branch, we get acc * x^{n} = acc * a^{(n-1) div 2}. Solving for a (again using the identity), we discover we're off by a factor of x. However, we can go back to our choice of c and change it to c = x * acc. This works out, leaving us with:
(* requires n >= 0 *) (* returns acc * x^n *) fun expRsTr(x, n, acc) = if n = 0 then acc else if n mod 2 = 0 then (* n is even *) expRsTr(x*x, n div 2, acc) else (* n is odd *) expRsTr(x*x, (n-1) div 2, x*acc)
We could now, if we wanted, derive a verification condition for expRsTr
.
The reasoning embodied in that vc would be what we just used informally.
Notice how having a specification for the (tail) recursive function---before
writing its code---was helpful. By assuming that specification held for
recursive calls, we were guided in deriving what arguments to pass to those
calls. And we were able to reason about each branch of the function
individually, without needing to think about what the other branches were
doing.