Spring 1996, COMP 204, Stotts
SOLUTION

1.  procedure Z(a,b):() {
      if a > 0 then {
         a := a - 1
         call Z(a,b)
         b := b * a
      }
    }

 We take a "guess" f and see if f is the correct function [Z].
 The Mills rule to show this for recursive procedures is
  
    [Z] = f iff
       i) dom(f) = dom([Z])
       ii) f = (a>0 --> [a := a-1] o f o [b := b*a]) | (a<=0 --> Ident)

 Let's guess 
 
           --
           | a, b := 0, 0   if a > 0
      f = -|
           | identity       otherwise
           --

      or stated otherwise,

      (a>0 --> a,b := 0,0 ) | (T --> a,b := a,b)

 i) Here, dom([Z]) is the set of inputs for which the procedure
    terminates... which is all values of a, b.  If a <= 0, it
    terminates immediately.  If a >0, it recurses, but decrements 
    a by one each time, eventually hitting 0 causing the recursion
    to terminate

    In our "guess" f, the two clauses are defined over all values 
    a,b so the two domains are the same.

 ii) Plug in all functions, do the compositions, simplify:

     trace table 1

       statement   condition     a        b

        if          a>0
       a := a-1                 a-1
         Z(a,b)     a-1>0        0        0
       b := b*a                          0*0
      -----------------------------------------------
          (a>0 and a>1 --> a,b := 0,0)

     trace table 2

       statement   condition     a        b
 
         if         a>0
       a := a-1                 a-1
         Z(a,b)     a-1<=0                     
       b := b*a                         b*(a-1)
      -----------------------------------------------
            (a>0 and  a<=1 -->   a,b := a-1, b*(a-1))
         or (a=1 --> a,b := 0,0)


     trace table 3

       statement   condition     a        b
 
         if         a<=0         a        b
     -------------------------------------------------
         (a<=0 --> ident)
  
    So total function is
    
       (a>0 --> a,b := 0,0) | ()


    which is f.  So condition (ii) holds.


=============================================================================
2.

  There are two loops, so we need two invariants.
  We can allow some informality, abbreviations, etc. in order to
  succinctly express the abstract concepts manipulated by the loop.

  First, rewrite the repeat loop to make it a while

     s:= 2;

     if p[s] {
       t := s+s;
       while t <= m { p[t], t := FALSE, t+s }
     }
     s := s+1;
  
     while s <> m {
       if p[s] {
         t := s+s;
         while t <= m { p[t], t := FALSE, t+s }
       }
       s := s+1;
     }


  These are probably popular answers, but they do not contain enough 
  information to prove the POST condition:

     Invar for "while s <> m ..."
        forall 1 < k < s: p[k] == PRIME(k)

     Invar for "while t <= m ..."  
        forall s <= k < t : p[k] == PRIME(k) 

  This method of naming the invariants requires more work during
  proof to show that the actions in the loop bodies maintain the
  notion of "PRIME(k)" but that's an ok approach.



=============================================================================
3.

(a) new and add are used in the canonical form, so these are the 
    axioms to generate:

    set(n,v,new()) = new()
  
    set(n1,v1,add(n2,v2,A)) = ite(n1=n2, add(n1,v1,A), add(n2,v2,set(n1,v1,A)))

    del(n,new()) = new()

    del(n1,add(n2,v,A)) = ite(n1=n2, A, add(n2,v,del(n1,A))

    get(n,new()) = null

    get(n1,add(n2,v,A)) = ite(n1=n2, v, get(n1,A))


(b) Here is the normal form lemma:

    
    forall A in type AVL, there exists a k such that
      A = add(nk,vk,add(nk-1,vk-1,add(... (n1,v1,new()),...))

    or, forall A in type AVL, there exists a k such that NFL(A)


    proof: (we should accept some informality here, since the exam is short
      and the proof is tedious)

    Base case
      show it holds for all operations that have no arguments of type AVL
         NFL(new()) by definition, since we can let k=0.

    inductive step
      for all constructor operations "op" that take arguments "A" of 
      type AVL, show that if NFL(A) then NFL(op(A)). 

      i) NFL(A) ==> NFL(add(n,v,A))
         since NFL(A), we have some k for the number of add's in A.
         add(n,v,A) make that k+1, so we have NFL(add(n,v,A))
         with k+1.

      ii) NFL(A) ==> NFL(set(n,v,A))
          The effect of set is to find the first attribute "n"
          and change it's value to "v".  If there is no such "n"
          set has no effect, so set(n,v,A) = A, so NFL(set(n,v,A)).
          IF there is such an "n" then its value becomes v.  This
          is the same as not doing the last "add" in A, and instead
          doing an add with (n,v).  Hence, the number of add's
          in set(n,v,A) is k -1 +1 = k, so NFL(set(n,v,A).

      iii) NFL(A) ==> NFL(del(n,A)).
           Consider two cases: k=0 and k>0.
           k=0: here, A=new().  By definition, del(n,A) = new(),
             so NFL(del(n,A)).
           k>0: if n is in A< del effectively undoes one of the k adds, 
             so the resulting AVL consists of K-1 adds.  Hence
             NFL(del(n,A)). If n is not in A, del is a noop, so
             NFL(del(n,A)). 

      We conclude that only new and add are needed to construct any
      element A in AVL.