{ PRE: x0 = x and y0 = y } if (x > y) then y := x else x := y { POST: x = y = max(x0,y0) }
1) show { PRE and x > y } y := x { POST } { x = x = max(x0,y0) } y := x { POST } ax.assn. PRE and x > y ==> x0 = x and y0 = y and x0 > y0 arith. subst.