{ PRE: x > 3 } if ( x < 25 ) then x := 2 * x { POST: x >= 8 } 1) show { PRE and x < 25 } x := 2*x { POST } 2) show PRE and ~(x < 25) ==> POST 3) conclude { PRE } if ( x < 25 ) then x := 2*x { POST } by IF-THEN rule of inference QED