{ 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 } 2) show { PRE and ~(x > y) } x := y { POST } { y = y = max(x0,y0) } x := y { POST } ax.assn. PRE and ~(x > y) ==> x0 = x and y0 = y and x0 <= y0 arith. subst. ==> y = max(x0,y0) arith. subst. since y = y0 and y0 >= x0 so step 2) holds conseq. QED