prog

Dijkstra's Predicate Transfomer Semantics

14 2021-10-23 22:27

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