Slide 10.7: General properties of wp

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 := y², x = y and y > 0 )
 = wp( x := y², x = y ) and wp( x := y², 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 := y², x = y ) or wp( x := y², y > 0 )
 → wp( x := y², x = y or y > 0 )