CS312 Recitation 14
Verification conditions, using specs to write recursive functions

1. Verification conditions

   (* 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.

2. Tail recursion and Specifications
   1. Maximum element of list

      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.

   2. Exponentiation by repeated squaring

      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:

      xn =
       1 if n = 0
       (x2)n/2} if n is even
       x * (x2)^(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ⁿ. For the first branch, where n = 0, this means that we need to return acc * xⁿ, 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ⁿ. 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ⁿ = 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ⁿ = acc * a^{n div 2}. Solving for a (using the identity from before), we get a = x². 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ⁿ = 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.