Com S 641 --- Semantic Models of Programming Languages

	      HOMEWORK 3: States and State Transformers
		 (File $Date: 2002/03/11 20:02:55 $)

Due: Feb. 22, 2002.

The following are exercises from chapter 5 of Back and von Wright's book.
Please use the proof format described in chapter 4 for all of your
proofs, and do the proofs formally.  You may find it helpful to do
such proofs on the computer. 

1. (10 points) [5.1]
   Show that the following property follows from the independence assumptions:
      set.x.e.s == set.x.e'.s ==> e.s == e'.s

2. (10 points) [5.4]
   Prove the following property:
      (x,y := e1,e2) = (y,x := e2,e1).

3.  [5.5]
a. (10 points, extra credit)
   Verify the following using Corollary 5.2:
    (x*y).((x,y := x+y,y+1).s) == ((x+y)*(y+1)).s
b. (10 points)
   Verify the following using Corollary 5.2:
    (x*y).((z := x+y).s) == (x*y).s  



4. (15 points) [5.6]
   Use the properties of assignments to show the following equality:
      (z := x); (x,y := y,x) == (z := x); (x := y); (y := z)

5. (20 points) [5.8]
   When computing a sum, a local variable can be used to collect
   intermediate sums.  Show the following equality

     var x,y,z,s |-
         y := x + y + z
         == begin var s := 0; s := s + x; s := s + y; s := s + z; y := s end

6. (20 points) [5.9]
   Assume the following procedure definitions:

    Max(var x, val y,z) == x := max.y.z
    Min(var x, val y,z) == x := min.y.z

   where the operator max returns the greater of its two arguments and
   min returns the smaller.  Prove in full formal detail the following:

     Max(u,e,e'); u := e + e' - u  ==  Min(u,e,e')