Question 1-4

Provide a step-by-step partial correctness proof for the following. Justify each step with one of the three rules below, or ``algebraic fact'' if the conclusion is algebraically true and involves no assertions. 

{ z = xi }
z := z * x;
i := i + 1;
{ z = xi }

Solution

1. z = xi implies z * x = xi + 1
 (algebraic fact)

2. { z = xi }
   { z * x = xi + 1 }
 (consequence: 1)

3. { z * x = xi + 1 }
   z := z * x;
   { z = xi + 1 }
 (assignment)

4. { z = xi }
   z := z * x;
   { z = xi + 1 }
 (sequence: 3, 4)

5. { z = xi + 1 }
   i := i + 1;
   { z = xi }
 (assignment)

6. { z = xi }
   z := z * x;
   i := i + 1;
   { z = xi }
 (sequence: 4, 5)

Back to Review for Quiz 1