cse403 Homework#4 Due: Friday, May15, in class
1. The following code computes x=max(1,a,b), where a and b are integers.
x := a; if x<1 then x := 1;
while x<b do x := x + 1; end;
Prove that the loop invariant is
{ (x³ a) Ù (x³ 1) Ù ( x£ max(1, a, b) }
2. Derive a proof rule for the C do statement:
do S while (B ) ,
where S is a statement and B is a (Boolean) expression.
3. Following is a program segment that computes the result of raising a positive integer z to an integer power y.
{ z and y are positive integers.}
x := 1; j := 1;
while y _ j do
j := j + 1; x := x * z;
end loop;
{ x = z y }
Prove that it is correct by inserting assertional annotations between statements, such that the truth of the assertions follows directly from the axiom of assignment and proof rules.