Example 2: Proof Plan
OUTLINE OF PROOF
{ PRE: x0 = x and y0 = y }
if (x > y) then y := x
else x := y
{ POST: x = y = max(x0,y0) }
- show { PRE and x > y } y := x { POST }
- show { PRE and ~(x > y) } x := y { POST }
- conclude { PRE } if-then-else { POST }