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.
Using only the definition, and some abuse of notation we can trivially prove this:
Your "some abuse of notation" is in contradiction with non-determinism, where "S(w) in Q" is nonsensical. The essential part is that you have "subset of" instead of "element of". With this modification a moment of reflection will allow you to see that if 'C is a subset of (Q or R)' it does not follow that '(C is a subset of Q) or (C is a subset of R)', since C could be half here half there.
For example take C={1, 2, ... 10}, Q=evens, R=odds. Then Q or R is N, the naturals. Evidently C is a subset of N. Equally evidently, 'C is a subset of Q' and 'C is a subset of R' are both false.
But the whole w \in wp(S, Q or R) does not make any sense in itself, since the value of wp is a predicate, not a set. You failed to type-check your proof.
By the way Wikipedia has a counter-example, but I have trouble understanding it.
>>4
Oh right, I think I've got it. You have an S that randomly returns 0 or 1. Then wp(S, x=0 /\ x=1) = true, since it always happens regardless of initial state. But wp(S, x=0) and wp(S, x=1) will both be false since there's no initial state that will always satisfy the post-condition.
That was meant to be wp(S, x=0 \/ x=1) not wp(S, x=0 /\ x=1), sorry about that.
☡
non wlp(S, R)
| = ¬ 1
|| if S = M¬
|| R := true
|| fi
| = ¬ 2
|| if S = Mo ∨ (1)
|| fi
| = 3
|| if S = M¬ ∧ S = ¬R
|| fi
| = 4
|| wp(S, non R)
|| wlp(S, (non) R)
|| (R non ,S)pw
(R ,S)plw non>>2,4-6
Yes, this makes sense, thank you.
>>3
In my defense it does characterize a set. I guess that would be something like w \in {w | wp(S, Q or R)}.
>>7
I don't understand this... but I don't think I'm intended to.
>>8
err, something like w \in {w | (wp(S, Q or R))(w)}.
Is the book in question Predicate Calculus and Program Semantics?
I think that the answer to your second question is just that the negation of "for-all P" is not "for-all not P", but "exists not P".
>>8 ☡
>>11
Ah, I think I've got it now then. Do the following seem like accurate definitions then:
[wlp(S, R)](w) = \forall x \in S(w) : R(x)
[wp(S, R)](w) = \forall x \in S(w) : R(x) \wedge S(w) \not= \emptysetEvaluating the negation of our two operations we then have:
non [wlp(S,R)](w)
= non [\forall x \in S(w) : R(x)]
= \exists x \in S(w) : non R(x)non [wp(S,R)](w)
= non [\forall x \in S(w) : R(x) \wedge S(w) \not= \emptyset]
= non [\forall x \in S(w) : R(x)] \vee non [S(w) \not= \emptyset]
= \exists x \in S(w) : R(x) \vee S(w) = \emptyset>>13
No, this is wrong as well. Hopefully the following is correct:
[wlp(S, R)](w) = ∀ x ∈ S(w) : x = ∅ ∨ R(x)
[wp(S, R)](w) = ∀ x ∈ S(w) : x ≠ ∅ ∧ R(x)>>14
The definitions:
[wlp(S, R)](w) = \forall x \in S(w) : x = abort or R(x)
[wp(S, R)](w) = \forall x \in S(w) : x != abort and R(x)The negation of the definitions:
non [wlp(S, R)](w)
= non [\forall x \in S(w) : x = abort or R(x)]
= \exists x \in S(w) : x != abort and non R(x)non [wp(S, R)](w)
= non [\forall x \in S(w) : x != abort and R(x)]
= \exists x \in S(w) : x = abort or non R(X)The compound aspects of the state space of wlp:
ab. [wp(S, T) and non wlp(S, R) and non wlp(S, non R)](w)
= (\forall x \in S(w) : x != abort) and (\exists x \in S(w) : x != abort and non R(x)) and (\exists x \in S(w) : x != abort and R(x))
initial state determines proper termination but whether the final state satisfies R or non R is not determined.ac. [wlp(S, R) and non wp(S, T)](w)
= (\forall x \in S(w) : x = abort or R(x)) and (\exists x \in S(w) : x = abort)
initial state does not determine proper termination, but if it terminates properly its final state satisfies R.bc. [wlp(S, non R) and non wp(S, T)](w)
= (\forall x \in S(w) : x = abort or non R(x)) and (\exists x \in S(w) : x = abort)
initial state does not determine proper termination, but if it terminates properly its final state satisfies non R.abc. [non (wlp(S, R) or wlp(S, non R), or wp(S, T))](w)
= non wlp(S, R) and non wlp(S, non R) and non wp(S, T)
= (\exists x \in S(w) : x != abort and non R(x)) and (\exists x \in S(w) : x != abort and R(x)) and (\exists x \in S(w) : x = abort)
initial state does not determine proper termination or in the case of proper termination if the final state will satisfy R or non R.This is much better! My last question for now would then be why do we not need to show (\exists x \in S(w) : x != abort) in the ac. and bc. cases?
>>15
Good question. I think it is just wrong. If you look at the picture on page 22, the current formulas obviously overlap in c__. Therefore __ac should be wlp(S, R) and non wp(S, T) and non wlp(S, non R) and bc should be wlp(S, non R) and non wp(S, T) and non wlp(S, R), which matches the description and makes them mutually exclusive as promised.
>>16
This tracks to me, and in both cases the additional element simplifies to (\exists x \in S(w) : x != abort). While we've been discussing I've been reread to where I was before my hiatus. I haven't run into any more confusion, and in fact I feel I have a pretty solid understanding now. Thanks everyone!
Beyond the actual knowledge of the subject the main lessons learned were to pay special attention to deviations from the norm, such as the fact that a non-deterministic mechanism clearly isn't a function but a multifunction. Probably also trying explicitly to model things as they are instead of as I would like them to be (or not at all), would help.