Some properties of wp
Law of excluded miracle: wp(S,F) = F
Distributivity of conjunction: wp(S,Q) ?wp(S,R) = wp(S,Q ?R)
Law of monotonicity: if Q => R then wp(S,Q) => wp(S,R)
Distributivity of disjunction: wp(S,Q) ?wp(S,R) => wp(S,Q ? R)
Nondeterministic:
- Execution of a command is nondeterministic if it need not always be exactly the same each time it is begun in the same state
- e.g. {x = 4} x := 14 || x := x+1 {?}