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.