Predicate transformer semantics: Difference between revisions

Revision as of 11:23, 29 November 2022

Revision as of 11:24, 29 November 2022

Line 222:

=== Strict ===

A predicate transformer ''S'' is '''strict''' iff:

:<math>TS(\texttt{falseF})\ \Leftrightarrow\ \texttt{falseF}</math>

For instance, ''wp'' is artificially made strict, whereas ''wlp'' is generally not. In particular, if statement ''S'' may not terminate then