Consider this program fragment (assume we are using all integers):
{ PRE: x > 3 } if ( x < 25 ) then x := 2 * x { POST: x >= 8 }