Content deleted Content added
m →Strongest postcondition: Dark mode |
|||
| (5 intermediate revisions by 5 users not shown) | |||
Line 1:
{{Short description|Reformulation of Floyd-Hoare logic}}
{{Semantics}}
{{Semantics}}'''Predicate transformer semantics''' were introduced by [[Edsger W. Dijkstra|Edsger Dijkstra]] in his seminal paper "[[Guarded commands|Guarded commands, nondeterminacy and formal derivation of programs]]". They define the semantics of an [[imperative programming]] paradigm by assigning to each ''statement'' in this language a corresponding ''predicate transformer'': a [[total function]] between two ''[[predicate (mathematical logic)|predicates]]'' on the state space of the statement. In this sense, predicate transformer semantics are a kind of [[denotational semantics]]. Actually, in [[guarded commands]], Dijkstra uses only one kind of predicate transformer: the well-known '''weakest preconditions''' (see below).▼
▲
Moreover, predicate transformer semantics are a reformulation of [[Floyd–Hoare logic]]. Whereas Hoare logic is presented as a [[deductive system]], predicate transformer semantics (either by '''weakest-preconditions''' or by '''strongest-postconditions''' see below) are '''complete strategies''' to build [[Deductive reasoning|valid deductions]] of Hoare logic. In other words, they provide an effective [[algorithm]] to reduce the problem of verifying a Hoare triple to the problem of proving a [[First-order logic|first-order formula]]. Technically, predicate transformer semantics perform a kind of [[symbolic execution]] of statements into predicates: execution runs ''backward'' in the case of weakest-preconditions, or runs ''forward'' in the case of strongest-postconditions.
Line 12 ⟶ 14:
=== Skip ===
{|
|<math>wp(\texttt{skip},R) \ =\ R</math>
|}
=== Abort ===
{|
|<math>wp(\texttt{abort},R) \ =\ \texttt{F}</math>
|}
Line 24 ⟶ 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 30 ⟶ 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 45 ⟶ 47:
=== Sequence ===
{|
|<math>wp(S_1;S_2,R)\ =\ wp(S_1,wp(S_2,R))</math>
|}
Line 57 ⟶ 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 70 ⟶ 72:
=== While loop ===
==== Partial
Ignoring termination for a moment, we can define the rule for the ''weakest liberal precondition'', denoted ''wlp'', using a predicate ''
{|
|<math>wlp(\texttt{while}\ E\ \texttt{do}\ S\ \texttt{done}, R)\Leftarrow \ \textit{INV} \ \ \text{if} \ \
\begin{array}[t]{l}
Line 82 ⟶ 85:
|}
==== Total
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 100 ⟶ 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 116 ⟶ 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 143 ⟶ 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 155 ⟶ 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 198 ⟶ 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 208 ⟶ 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>
|}
Line 254 ⟶ 257:
:<math>S(P \vee Q)\ \Leftrightarrow\ S(P) \vee S(Q)</math>
This is generally not the case of <math>wp(S,.)</math> when ''S'' is non-deterministic. Indeed, consider a non-deterministic statement ''S'' choosing an arbitrary
:<math>S\ =\ \texttt{if}\ \texttt{true} \rightarrow x:=0\ [\!]\ \texttt{true} \rightarrow x:=1\ \texttt{fi}</math>
Line 273 ⟶ 276:
In predicate transformers semantics, expressions are restricted to terms of the logic (see above). However, this restriction seems too strong for most existing programming languages, where expressions may have side effects (call to a function having a side effect), may not terminate or abort (like ''division by zero''). There are many proposals to extend weakest-preconditions or strongest-postconditions for imperative expression languages and in particular for [[Monad (functional programming)|monads]].
Among them, ''Hoare Type Theory'' combines [[Hoare logic]] for a [[Haskell (programming language)|Haskell]]-like language, [[separation logic]] and [[type theory]].<ref>{{cite journal |first1=Aleksandar |last1=Nanevski |first2=Greg |last2=Morrisett |first3=Lars |last3=Birkedal |title=Hoare Type Theory, Polymorphism and Separation |journal=Journal of Functional Programming |volume=18 |issue=5–6 |pages=865–911 |date=September 2008 |doi=10.1017/S0956796808006953 |s2cid=6956622 |url=
This system is currently implemented as a [[Coq (software)|Coq]] library called '''Ynot'''.<ref>[http://ynot.cs.harvard.edu/ Ynot] a [[Coq (software)|Coq]] library implementing Hoare Type Theory.</ref> In this language, [[Evaluation strategy|evaluation of expressions]] corresponds to computations of ''strongest-postconditions''.
| |||