Homework 7

Due Thursday, April 13 at the start of class.

1. Write correctness proofs for the following procedures:

   1. procedure SUB1(in x; out y): (x>1) -> ((y>0) & (x>y))
      var a
      begin
        a := 1;
        y := x;
        y := y-a
      end
      

   2. procedure P(in x; out y): y=(x+1)
      var a
      begin
        a := x+1;
        if (a-1)=0
          then
            y := 1
          else
            y := a
        endif
      end
      

   3. procedure COPY2(in x; out y): y=x
      begin
        y := 0;
        while -(y=x)
          y := y+1
        endwhile
      end
      

2. Code an implementation for the following specification and prove it correct:

   procedure Q(in x; out y): ((x=0) -> (y=0)) & (-(x=0) -> (y=1))