{ 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.