Predicate transformer semantics: Difference between revisions

Revision as of 14:08, 22 July 2023

Revision as of 14:13, 22 July 2023

Line 83:

==== Total Correctness ====

To show total correctness, we also have to show that the loop terminates. For this we define a [[well-founded relation]] on the state space denoted as (wfs, <) and define a variant function '' vf '' , such that we have:

{| style="background-color:#eeeeff;" border="1" cellpadding="10"

|<math>wp(\texttt{while}\ E\ \texttt{do}\ S\ \texttt{done}, R)\ \Leftarrow \ \textit{INV} \ \ \text{if} \ \ \ \

\begin{array}[t]{l}

\\ (E \wedge \textit{INV} \Rightarrow \textit{vf} \in wfs) \\

\wedge\ (E \wedge \textit{INV} \wedge v=vf \Rightarrow wp(S,\textit{INV} \wedge v < \textit{vf})) \\

\wedge\ (\neg E \wedge \textit{INV} \Rightarrow R)

\end{array}</math>

Line 95:

Informally, in the above conjunction of three formulas:

* the first one means that the variant must be part of the well-founded relation before entering the loop;

* the second one means that the body of the loop (i.e. statement ''S'') must preserve the \textit{INV}ariantinvariant and reduce the variant;

* the last one means that the loop postcondition ''R'' must be established when the loop finishes.