{ PRE: x > 3 } if ( x < 25 ) then x := 2 * x { POST: x >= 8 }
1) show { PRE and x < 25 } x := 2*x { POST } { 2*x >= 8 } x := 2*x { x >= 8 } ax.assn. { x >= 4 } x := 2*x { x >= 8 } conseq. since x >= 4 ==> 2*x >= 8 { x > 3 } x := 2*x { x >= 8 } conseq. since x > 3 ==> x >= 4 int. arith. { x > 3 and x < 25 } x := 2*x { x >= 8 } conseq. since x > 3 and x < 25 ==> x > 3 QED