Assignment 3: Assigned October 3, due Monday, October 31 at 8:30am
  1. Fill in the missing precondition or postcondition to form a Hoare triple that is satisfied under partial correctness. For postconditions, make sure the formula expresses as much information as possible. (You do not need to provide proofs.)
    a. (| ?? |) z=z+y-1; (| z >= y |)
    b. (| ?? |) x=x+1; (| x=y |)
    c. (| a=9 |) a=2; b=a+1; a=b*b; (| ?? |)
    d. (| i=-j |) i=i+1; j=j-1; (| ?? |)
    e. (| ?? |) if (z==0) {x=z+1;} else {x=z-2;} (| x=1 |)

  2. p.300, 4.3 (1b)
  3. p.300, 4.3 (5b)
  4. Write down a program P such that (| T |) P (| a < (b - 2) + c |). (You do not need to provide a proof.)
  5. p.301, 4.3 (11a)
  6. p.301, 4.3 (14)
  7. p.303, 4.4 (1a) (Please see p.301, 4.3 (13) for the definition of Copy1.)