CSE526: Principles of Programming Languages
			      Scott Stoller
			   hw3: Hoare logic
			version: 5pm,1feb2004
			   due: 26 feb 2004

1. Prove correctness of the following program for computing integer
square roots in linear time.  Specifically, prove

{ x >= 0 }
r := 0;
while x >= (r+1)^2 do r := r+1
{ r^2 <= x < (r+1)^2 }

As indicated on [Reynolds, page 57], you do not need to prove
predicate-logic assertions (such as x < x+1) that occur in the proof,
but the assertions should be valid.

You may structure your proof in the linear format described in
[Reynolds, chapter 3] or as a proof tree (if you are comfortable with
that concept).