Predicate transformer semantics: Difference between revisions

Revision as of 14:13, 22 July 2023

Revision as of 14:15, 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 ({{mvar|wfs}}, <) and define a variant function ''{{mvar|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 \textit{wfs}) \\

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

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

\end{array}</math>

where ''{{mvar|v''}} is a fresh tuple of variables

|}

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 ''{{mvar|S''}}) must preserve the invariant and reduce the variant;

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

However, the conjunction of those three is not a necessary condition. Exactly, we have