Predicate transformer semantics: Difference between revisions

Revision as of 11:20, 29 November 2022

Revision as of 11:23, 29 November 2022

Line 215:

=== Monotonic ===

Predicate transformers of interest (''wp'', ''wlp'', and ''sp'') are [[monotonic]]. A predicate transformer ''TS'' is '''monotonic''' if and only if:

:<math>(\forall x,: P \Rightarrow: Q) \Rightarrow (\forall x,: S(P): \Rightarrow TS(Q))</math>

This property is related to the [[Hoare logic#Consequence rule|consequence rule of Hoare logic]].