April 23, 2001

Reading material

Pages 115-119.

Additional material

A draft version of a note on Hoare's proof system: PostScript and PDF. This note will hopefully be expanded soon.

Question

Give a proof using Hoare's proof system of

{ y = oldY }
x = x + y;
y = y - x;
if (x + y > 0) 
    y = x + y; 
else
    y = -x - y;
{ x = oldX + oldY and ((oldY > 0 and y = oldY) or (oldY <= 0 and y = -oldY)) }