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 )