Predicate transformer semantics: Difference between revisions

Revision as of 11:28, 29 November 2022

Revision as of 11:30, 29 November 2022

Line 233:

=== Terminating ===

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

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

Actually, this terminology makes sense only for strict predicate transformers: indeed, <math>wp(S,\texttt{true})</math> is the weakest-precondition ensuring termination of ''S''.