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

18


VIP:

do not edit these