General Properties of wp


The predicate transformer wp(C, Q) has certain properties.

Law of the Excluded Miracle
   wp( C, false ) = false
This states that nothing a programming construct C can do will make false into true—if it did it would be a miracle! For example,
   wp( x := x + 1, 1 < 0 ) = ( 1 < 0 )
Distributivity of Conjunction
   wp( C, P and Q ) = wp( C, P ) and wp( C, Q )
This property concerns the behavior of wp with regard to the “and” operator of logic (also called conjunction). For example,
   wp( x := y2, x = y and y > 0 )
 = wp( x := y2, x = y ) and wp( x := y2, y > 0 )
Law of Monotonicity
   if  Q → R  then  wp( C, Q ) → wp( C, R )
It regards the implication operator ‘→’. For example,
   if  x > 0 → x ≠ 0
     then  wp( x := x + 1, x > 0 ) → wp( x := x + 1, x ≠ 0 )
Distributivity of Disjunction
   wp( C, P ) or wp( C, Q ) → wp( C, P or Q )
with equality if C is deterministic. For example,
   wp( x := y2, x = y ) or wp( x := y2, y > 0 )
 → wp( x := y2, x = y or y > 0 )