[ prog / sol / mona ]

prog


Dijkstra's Predicate Transfomer Semantics

16 2021-10-24 09:52

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

18


VIP:

do not edit these