Predicate transformer semantics: Difference between revisions

Revision as of 11:11, 29 November 2022

Revision as of 11:20, 29 November 2022

Line 212:

== Predicate transformers properties ==

This section presents some characteristic properties of predicate transformers.<ref>{{cite book |first1=Ralph-Johan |last1=Back |first2=Joakim |last2=Wright |title=Refinement Calculus: A Systematic Introduction |url=https://books.google.com/books?id=cAEMCAAAQBAJ |orig-year=1978 |year=2012 |publisher=Springer |isbn=978-1-4612-1674-2 |series=Texts in Computer Science }}</ref> Below, ''TS'' denotes a predicate transformer (a function between two predicates on the state space) and ''P'' a predicate. For instance, ''TS(P)'' may denote ''wp(S,P)'' or ''sp(S,P)''. We keep ''x'' as the variable of the state space.

=== Monotonic ===

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

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

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

=== Strict ===

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

:<math>T(\texttt{false})\ \Leftrightarrow\ \texttt{false}</math>