本blog是针对Dijkstra的书A discipline of programming的第3章The characterization of semantics的读书笔记。
第19页的PROPERTY 4，4'比较confusing at first。我们可以在逻辑上进一步分解本章中的概念：
Let s be a state of the system. Let P be a predicate. Denote the true value of P on state s by Ps (think it as "P applied on s"). Let = denotes logical equivalence. Define predicate "Q⇒R" as: (Q⇒R)s = Qs→Rs (→ being the logic implication operator). Define predicate "Q or R" as: (Q or R)s = Qs∨Rs (∨ being the logic or operator). Define "Q and R" correspondingly. Denote the final state reached by machine S starting on initial state i by S(i). By the definition of the weakest precondition wp(S, R)s = RS(s). Equipped these notations, a formal proof of Property 3 can be conducted, which aids understanding of this property.
Proof of (wp(S, Q) and wp(S, R)) = wp(S, Q and R):
(wp(S, Q) and wp(S, R))s = wp(S, Q)s ∧ wp(S, R)s = QS(s) ∧ RS(s)
and
wp(S, Q and R)s = (Q and R)S(s) = QS(s) ∧ RS(s)
hence they are equal.
In the same way, Property 4, or (wp(S, Q) or wp(S, R)) = wp(S, Q or R) can be proved. Then the question is why Property 4 is a one-way implication? The key is to realize that in the above proof, we assumed S(s) is a single state, since we only defined the true value of a predicate on a single state. This means all the arguments holds only for deterministic machine. To deal with nondeterministic machine, first let S(i) be the set of possible final states reached from initial state i. Then we must define PW, in which P is a predicate and W is a set of states. Because a nondeterministic machine from a initial state i may produce any one of its possible final states in S(i), in order for a predicate to be true, all the final states must statisfies it. Thus: PW = ∀s∈W, Ps. Based on this definition P(W1∪W2) = PW1 ∧ PW2 (Note on the left-hand side is the set union, but on the right is the logic and, instead of or!). Now let's see why we have one-way implication in Property 4:
Suppose S(s) = {s1, s2, ... sn}. On the left-hand side:
(wp(S, Q) or wp(S, R))s = wp(S, Q)s ∨ wp(S, R)s = QS(s) ∨ RS(s) = Q{s1, s2, ... sn} ∨ R{s1, s2, ... sn} = (Qs1 ∧ Qs2 ∧ ... ∧Qsn) ∨ (Rs1 ∧ Rs2 ∧ ... ∧Rsn)
On the right-hand side:
wp(S, Q or R)s = (Q or R)S(s) = (Q or R){s1, s2, ... sn} = (Q or R)s1 ∧ (Q or R)s2 ∧ ... ∧(Q or R)sn = (Qs1 ∨ Rs1) ∧ (Qs2 ∨ Rs2) ∧ ... ∧ (Qsn ∨ Rsn)
Using propositional logic, we know the left-hand side ⇒ the right-hand side but not the other way round.
Finally, note if all ∨s are replaced by ∧s on both sides, they become equal, due to commutativity and associativity of the ∧ operator, which mean property 3 still holds for nondeterministic machines.