Predicate transformer semantics: Difference between revisions

Revision as of 11:33, 29 November 2022

Revision as of 11:35, 29 November 2022

Line 247:

=== Disjunctive ===

A predicate transformer ''TS'' is '''disjunctive''' iff:

:<math>TS(P \vee Q)\ \Leftrightarrow\ (TS(P) \vee TS(Q))</math>

This is generally not the case of <math>wp(S,.)</math> when ''S'' is non-deterministic. Indeed, consider a non-deterministic statement ''S'' choosing an arbitrary boolean. This statement is given here as the following ''selection statement'':

Line 259:

Whereas, the formula <math>wp(S, x=0) \vee wp(S,x=1)</math>

reduces to the ''wrong proposition'' <math>(0=0 \wedge 1=0) \vee (1=0 \wedge 1=1)</math>.

The same counter-example can be reproduced using a ''specification statement'' (see above) instead:

:<math>S\ =\ \texttt{true}\ |</math>&nbsp;@<math>y.\ y \in \{ 0, 1 \} \rightarrow x:=y</math>

== Applications ==