Content deleted Content added
m WP:ADOPTYPO boolean -> Boolean |
m →Strongest postcondition: Dark mode |
||
| (One intermediate revision by the same user not shown) | |||
Line 14:
=== Skip ===
{|
|<math>wp(\texttt{skip},R) \ =\ R</math>
|}
=== Abort ===
{|
|<math>wp(\texttt{abort},R) \ =\ \texttt{F}</math>
|}
Line 26:
We give below two equivalent weakest-preconditions for the assignment statement. In these formulas, <math>R[x \leftarrow E]</math> is a copy of ''R'' where [[Free variables and bound variables|free occurrences]] of ''x'' are replaced by ''E''. Hence, here, expression ''E'' is implicitly coerced into a ''valid term'' of the underlying logic: it is thus a ''pure'' expression, totally defined, terminating and without side effect.
* version 1:
{|
|<math> wp(x := E, R)\ =\ (\forall y. y = E \Rightarrow R[x \leftarrow y])</math>
where ''y'' is a fresh variable and not free in E and R (representing the final value of variable ''x'')
Line 32:
* version 2:
Provided that '' E '' is well defined, we just apply the so-called ''one-point'' rule on version 1. Then
{|
| <math> wp(x := E, R)\ =\ R[x \leftarrow E] </math>
|}
Line 47:
=== Sequence ===
{|
|<math>wp(S_1;S_2,R)\ =\ wp(S_1,wp(S_2,R))</math>
|}
Line 59:
=== Conditional ===
{|
|<math>wp(\texttt{if}\ E\ \texttt{then}\ S_1\ \texttt{else}\ S_2\ \texttt{end},R)\ =\ (E \Rightarrow wp(S_1,R)) \wedge (\neg E \Rightarrow wp(S_2,R))</math>
|}
Line 75:
==== Partial correctness ====
Ignoring termination for a moment, we can define the rule for the ''weakest liberal precondition'', denoted ''wlp'', using a predicate ''INV'', called the [[Loop invariant|Loop ''INV''ariant]], typically supplied by the programmer:
{|
|<math>wlp(\texttt{while}\ E\ \texttt{do}\ S\ \texttt{done}, R)\Leftarrow \ \textit{INV} \ \ \text{if} \ \
\begin{array}[t]{l}
Line 87:
==== 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:
{|
|<math>wp(\texttt{while}\ E\ \texttt{do}\ S\ \texttt{done}, R)\ \Leftarrow \ \textit{INV} \ \ \text{if} \ \ \ \
\begin{array}[t]{l}
Line 103:
However, the conjunction of those three is not a necessary condition. Exactly, we have
{|
|<math>wp(\texttt{while}\ E\ \texttt{do}\ S\ \texttt{done}, R)\ \ = \ \ \text{the strongest solution of the recursive equation} \
\begin{array}[t]{l}
Line 119:
==== Selection ====
Selection is a generalization of '''if''' statement:
{|
|<math>wp(\texttt{if}\ E_1 \rightarrow S_1 \ [\!] \ \ldots\ [\!]\ E_n \rightarrow S_n\ \texttt{fi}, R)\ = \begin{array}[t]{l}
(E_1 \vee \ldots \vee E_n) \\
Line 146:
The specification statement appears like a primitive in the sense that it does not contain other statements. However, it is very expressive, as ''pre'' and ''post'' are arbitrary predicates. Its weakest precondition is as follows.
{|
|<math>wp(x:l[pre, post], R) = (\exists l:: pre) \wedge (\forall s: (\forall l : pre : post(x \leftarrow s)) :
R(x \leftarrow s)) </math>
Line 158:
Formalization of jump statements like ''{{mono|goto}} L'' takes a very long bumpy process. A common belief seems to indicate the goto statement could only be argued operationally. This is probably due to a failure to recognize that ''{{mono|goto}} L'' is actually miraculous (i.e. non-strict) and does not follow Dijkstra's coined Law of Miracle Excluded, as stood in itself. But it enjoys an extremely simple operational view from the weakest precondition perspective, which was unexpected. We define
{|
|<math>wp(\texttt{goto}\ L, R) = wpL</math>
where ''wpL'' is the weakest precondition at label ''L''.
Line 201:
For example, on assignment we have:
{|
|<math> sp(x := E, R)\ =\ \exists y, x=E[x \leftarrow y] \wedge R[x \leftarrow y]</math>
where ''y'' is fresh
Line 211:
On sequence, it appears that ''sp'' runs forward (whereas ''wp'' runs backward):
{|
|<math>sp(S_1;S_2\ ,\ R)\ =\ sp(S_2,sp(S_1,R))</math>
|}
| |||