I recently posted some Dijkstra, and it reminded me to take a look again at predicate transformer semantics. I remember struggling with this before, and couldn't help but question Dijkstras choices at a few points. This was so bad as to have to put the book down, but I wouldn't be surprised if I was in the wrong. Either way I'd like to have some feedback. Recall the definition of weakest precondition:
Given some mechanism (S), and a post-condition (R), the weakest pre-condition corresponding to the post-condition (wp(S, R)) is the condition that characterizes the set of all initial mechanism states such that it necessarily properly terminates in a final state satisfying the post-condition.
Now Dijkstra claims that if S is a non-deterministic mechanism then wp(S, Q or R) => wp(S, Q) or wp(S, R) doesn't hold, but nothing in the definition claims anything to do with deterministic systems. Using only the definition, and some abuse of notation we can trivially prove this:
w \in wp(S, Q or R) => S(w) \in Q or R => S(w) \in Q or S(w) \in R => w \in wp(S, Q) or wp(S, R)
Something else that annoyed me is that negation of predicate-transformers is completely different from normal predicates, and in fact the negation of a predicate transform is equivalent to T. Can negation of predicate transfomers be removed entirely, or is this used for some task? Is there a more concise explanation of what exactly these predicate transformers are? What follows are the negation of two predicate transformers, the first treating it as a predicate, and the second what inductively seems to be used in the text:
non wlp(S, R)
= not (if S terminates then it satisfies R.)
= not (S doesn't terminates or it terminates satisfying R.)
= S terminates and doesn't satisfy R.
= wp(S, non R)non wlp(S, R)
= not promise (if S terminates then it satisfies R)
= maybe (if S terminates then it satisfies R)
= T (aka. null statement)I removed all the negated predicate transformers from the description of the statespace of wlp, and not only did it seem to retain meaning, but it seemed drammatically more understandable.