[ prog / sol / mona ]

prog


Dijkstra's Predicate Transfomer Semantics

2 2021-10-22 20:55

>>1

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.

4 2021-10-22 22:16 *

By the way Wikipedia has a counter-example, but I have trouble understanding it.

5 2021-10-22 22:22

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

6 2021-10-22 22:23 *

That was meant to be wp(S, x=0 \/ x=1) not wp(S, x=0 /\ x=1), sorry about that.

18


VIP:

do not edit these