{ 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 } 3) conclude { PRE } if (x > y) then y := x else x := y { POST } by IF-THEN-ELSE rule of inference QED