>>14
The definitions:
[wlp(S, R)](w) = \forall x \in S(w) : x = abort or R(x)
[wp(S, R)](w) = \forall x \in S(w) : x != abort and R(x)The negation of the definitions:
non [wlp(S, R)](w)
= non [\forall x \in S(w) : x = abort or R(x)]
= \exists x \in S(w) : x != abort and non R(x)non [wp(S, R)](w)
= non [\forall x \in S(w) : x != abort and R(x)]
= \exists x \in S(w) : x = abort or non R(X)The compound aspects of the state space of wlp:
ab. [wp(S, T) and non wlp(S, R) and non wlp(S, non R)](w)
= (\forall x \in S(w) : x != abort) and (\exists x \in S(w) : x != abort and non R(x)) and (\exists x \in S(w) : x != abort and R(x))
initial state determines proper termination but whether the final state satisfies R or non R is not determined.ac. [wlp(S, R) and non wp(S, T)](w)
= (\forall x \in S(w) : x = abort or R(x)) and (\exists x \in S(w) : x = abort)
initial state does not determine proper termination, but if it terminates properly its final state satisfies R.bc. [wlp(S, non R) and non wp(S, T)](w)
= (\forall x \in S(w) : x = abort or non R(x)) and (\exists x \in S(w) : x = abort)
initial state does not determine proper termination, but if it terminates properly its final state satisfies non R.abc. [non (wlp(S, R) or wlp(S, non R), or wp(S, T))](w)
= non wlp(S, R) and non wlp(S, non R) and non wp(S, T)
= (\exists x \in S(w) : x != abort and non R(x)) and (\exists x \in S(w) : x != abort and R(x)) and (\exists x \in S(w) : x = abort)
initial state does not determine proper termination or in the case of proper termination if the final state will satisfy R or non R.This is much better! My last question for now would then be why do we not need to show (\exists x \in S(w) : x != abort) in the ac. and bc. cases?