Assignment 3:Assigned October 3, due Monday, October 31 at 8:30am

- 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 |)

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