Content deleted Content added
mNo edit summary |
→Conditional: add while loop |
||
Line 46:
As example:
:<math>wp(\textbf{if}\ x < y\ \textbf{then}\ x:=y\ \textbf{else}\ \textbf{skip}\ \textbf{endif},\ x \geq y)\ =\ (x < y \Rightarrow wp(x:=y,x\geq y)) \wedge (\neg x<y \Rightarrow x \geq y)\ =\ (x < y \Rightarrow y\geq y)\ =\ \textbf{true}</math>
=== While loop ===
Weakest-precondition of ''while-loop'' is usually parametrized by a predicate ''I'' called [[loop invariant]], and a [[well-founded relation]] on the space state denoted "<math><</math>" and called [[loop variant]]. More formally, we denote <math>\vec{x}</math> the [[tuple]] of variables involved in the statement, we have
<math>wp(\textbf{while}\ E\ \textbf{do}\ S\ \textbf{done}, R)\ =\
\begin{array}[t]{l}
I\\
\wedge\ \forall \vec{x_0}, ((E \wedge I) \Rightarrow wp(S,I \wedge \vec{x_0} < \vec{x}))[\vec{x} \leftarrow \vec{x_0}]\\
\wedge\ \forall \vec{x_0}, ((\neg E \wedge I) \Rightarrow R)[\vec{x} \leftarrow \vec{x_0}]
\end{array}\ </math>
where <math>\vec{x_0}</math> is a fresh tuple of variables.
In theory, we may build ''invariant'' and ''variant'' using a technique similar to [[Kleene fixed-point theorem]]. Below, we sketch this construction in [[set theory]]. We assume that ''U'' is a set denoting the state space. First, we define a family of subsets of ''U'' denoted <math>(A_k)_{k \in \mathbb{N}}</math> by induction over [[Natural number]] ''k''. Informally <math>A_k</math> represents the set of reachable states after ''k'' backward iteration of the loop:
* <math>A_0\ =\ \emptyset </math>
* <math>A_{k+1}\ =\ \{ \vec{x_0} \in U\ | \ ((E \Rightarrow wp(S, \vec{x} \in A_k)) \wedge (\neg E \Rightarrow R))[\vec{x} \leftarrow \vec{x_0}] \} </math>
Then, we define:
* invariant ''I'' as the predicate <math>\exists k, x \in A_k</math>.
* [[ Termination analysis | measure ]] ''m'' as the function <math>m: \vec{x} \mapsto \min \{ k | A_k \cap \{ \vec{x} \} \neq \emptyset \}</math>.
* variant <math>\vec{x_0} <\vec{x}</math> as the proposition <math>m(\vec{x_0}) > m(\vec{x})</math>
With these definitions, <math>wp(\textbf{while}\ E\ \textbf{do}\ S\ \textbf{done}, R)</math> reduces to formula <math>\exists k, x \in A_k</math>.
However on practical examples, such an abstract construction can not be handled efficiently by theorem provers. Hence, loop invariants and variants are provided by human users, or are inferred by some static analysis.
=== Weakest-preconditions of [[Guarded commands]] ===
| |||