Homework #1 (Part I): CSE503, Winter 2002

1. (20 points total)  Determine the weakest logical property Z that will make each of the following Hoare triples hold true
   1. {x + y > 10} x := y; y := 3 {Z}
   2. {Z} x:=3·x {x>0}
   3. {Z}if a > b then m := a else m := b {m=max(a,b)}
   4. {Z} x := 2*x*y {x+y < 64}
      
2. (10 points) Write pre- and postconditions for a specification intended to start with the integers a and b, ensuring that the maximum of these two integers is left in variable m when the program terminates.
   
3. (20 points total) Prove the following program is correct, including termination:
   {n > 0}
   s := 0;
   i := 0;
   while i<n do
       s := s + i;
       i = i + 1
   end;
   {s = n*(n-1)/2}
   
4. (10 points) Is the following Hoare triple weakly-correct, strongly-correct, or incorrect?  Justify your answer.
   {true} while 3 < 4 do x := x + 1  {3 = 4}
   
5. (40 points total) Consider the following abstract data type:
   type Set {
       private elements = {};
       public void insert (int x) { post == if isMember(x) then
                                               elements' = elements
                                            else elements' = elements union {x} };
       public void delete(int x) { post == if isMember(x) then
                                               elements' = elements \ {x}
                                           else elements' = elements }
       public int size() { post == length(elements) }
   }
   1. (5 points) Define an appropriate abstraction invariant for Set?
   2. (5 points) Sketch an implementation for Set that uses a (Java-like) vector to represent the set.
   3. (5 points) Define an appropriate concrete (implementation) invariant for Set?
   4. (10 points) Define an appropriate abstraction function that relates the implementation and the abstraction for Set.
   5. (15 points) Sketch a proof of correctness of the Set abstract data type as implemented by your implementation in 5B.