Question 0-11

Prove the following using the axiomatic scheme below. You may justify true mathematical assertions by writing only ``mathematical fact.''

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

Solution

1. z = xⁱ implies z * x = x^{i + 1}
 (algebraic fact)

2. { z = xⁱ }
   { z * x = x^{i + 1} }
 (consequence: 1)

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

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

5. { z = x^{i + 1} }
   i := i + 1;
   { z = xⁱ }
 (assignment)

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

Back to Exam 0