Exercises

1. Do Ex. 2.7 from [Win].
   
   
2. Consider the following relation between arithmetic expressions of IMP:
   a R a'
   iff
   there is an n in N such that for all &sigma in Sigma, <a, &sigma> -> n iff <a', &sigma> -> n.
   
   Prove that R is not an equivalence relation.
   
   
3. Prove that
   for all X in Loc and c in Com, skip ~ while not(X=X) do c.
   
   
4. Do Ex. 3.5, 3.6, and 3.8(1) from [Win].
   
   
5. Do Ex. 4.3 and 4.4 from [Win].
   
   
6. Complete the proof of Prop. 4.7 in [Win] by proving the missing cases.
   
   
7. Show by structural induction on arithmetic expressions that the relation A[[a]], as defined in [Win], is a total function for all arithmetic expressions a.
   
   
8. Show by structural induction on Boolean expressions that the relation B[[b]], as defined in [Win], is a total function for all Boolean expressions b.
   
   
9. Complete the proof seen in class of Lemma 5.4 by proving the missing cases.
   
   
10. Use the your completed proof of Lemma 5.4 as a model to prove Lemma 5.3.
    
    
11. Complete the proof seen in class of Theorem 5.7 by proving the missing cases.
    
    
12. Do Ex. 5.9(i) from [Win].
    
    
13. Do Ex. 6.5 and 6.15 from [Win].
    
    
14. Prove the following partial correctness assertion { true } R := X; Q := 0; while Y <= R do (R := R-Y; Q := Q+1) { X = (Q x Y) + R   /\  R < Y}