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