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.
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.