Content deleted Content added
m →Total Correctness: \text |
m →While loop: \text |
||
Line 71:
=== While loop ===
==== Partial Correctness ====
Ignoring termination for a moment, we can define the rule for the ''weakest liberal precondition'', denoted ''wlp'', using a predicate ''\textit{INV}'', called the [[loop
{| style="background-color:#eeeeff;" border="1" cellpadding="10"
|<math>wlp(\texttt{while}\ E\ \texttt{do}\ S\ \texttt{done}, R)\Leftarrow \ \textit{INV} \ \ \text{if} \ \
\begin{array}[t]{l}
\\ (E \wedge \textit{INV} \Rightarrow wlp(S,\textit{INV}))\\
\wedge\ (\neg E \wedge \textit{INV} \Rightarrow R)
\end{array}
</math>
Line 85:
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 vf \in wfs) \\
\wedge\ (E \wedge \textit{INV} \wedge v=vf \Rightarrow wp(S,\textit{INV} \wedge v < vf)) \\
\wedge\ (\neg E \wedge \textit{INV} \Rightarrow R)
\end{array}</math>
where ''v'' is a fresh tuple of variables
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
* the last one means that the loop postcondition ''R'' must be established when the loop finishes.
Line 102:
{| style="background-color:#eeeeff;" border="1" cellpadding="10"
|<math>wp(\texttt{while}\ E\ \texttt{do}\ S\ \texttt{done}, R)\ \ = \ \ \text{the strongest solution of the recursive equation} \
\begin{array}[t]{l}
Z: [Z\equiv(E\wedge wp(S, Z)) \vee (\neg E \wedge R)]
| |||