Content deleted Content added
m →Goto statement: {{mono}} {{tmath}} |
m →Strongest postcondition: Dark mode |
||
| (12 intermediate revisions by 11 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 6 ⟶ 8:
== Weakest preconditions ==
=== Definition ===
For a statement ''S'' and a [[postcondition]] ''R'', a '''weakest precondition''' is a predicate ''Q'' such that for any [[precondition]] {{mvar|P}}, <math>\{ P \} S \{ R \}</math> if and only if <math> P \Rightarrow Q </math>. In other words, it is the "loosest" or least restrictive requirement needed to guarantee that ''R'' holds after ''S''. Uniqueness follows easily from the definition: If both ''Q'' and ''Q' '' are weakest preconditions, then by the definition <math>\{ Q' \} S \{ R \}</math> so <math> Q' \Rightarrow Q </math> and <math>\{ Q \} S \{ R \}</math> so <math> Q \Rightarrow Q' </math>, and thus <math> Q=Q' </math>. We often use <math>wp(S, R)</math> to denote the weakest precondition for statement ''S'' with
=== Conventions ===
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
{|
|<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
|}
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
* the last one means that the loop postcondition
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 237 ⟶ 240:
=== Terminating ===
A predicate transformer ''S'' is '''terminating'''
:<math>S(\texttt{T})\ \Leftrightarrow\ \texttt{T}</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 267 ⟶ 270:
* Computations of weakest-preconditions are largely used to statically check [[Assertion (computing)|assertions in programs]] using a theorem-prover (like [[satisfiability modulo theories|SMT-solvers]] or [[Interactive theorem proving|proof assistants]]): see [[Frama-C]] or [[ESC/Java|ESC/Java2]].
* Unlike many other semantic formalisms, predicate transformer semantics was not designed as an investigation into foundations of computation. Rather, it was intended to provide programmers with a methodology to develop their programs as "correct by construction" in a "calculation style". This "top-down" style was advocated by Dijkstra<ref>{{cite journal |first=Edsger W. |last=Dijkstra |title=A Constructive Approach to the Problem of Program Correctness |journal=BIT Numerical Mathematics |volume=8 |issue=3 |pages=174–186 |year=1968 |doi= 10.1007/bf01933419|s2cid=62224342 }}</ref> and [[Niklaus Wirth|N. Wirth]].<ref>{{cite journal |author-link=Niklaus Wirth |first=N. |last=Wirth |title=Program development by stepwise refinement |journal=Comm. ACM |volume=14 |issue=4 |pages=221–7 |date=April 1971 |doi=10.1145/362575.362577 |hdl=20.500.11850/80846 |s2cid=13214445 |url=http://e-collection.library.ethz.ch/eserv/eth:3026/eth-3026-01.pdf |hdl-access=free }}</ref> It has been formalized further by [[Ralph-Johan Back|R.-J. Back]] and others in the [[refinement calculus]]. Some tools like [[B-Method]] now provide [[automated reasoning]] in order to promote this methodology.
* In the meta-theory of [[Hoare logic]], weakest-preconditions appear as a key notion in the proof of [[Gödel's completeness theorem|relative completeness]].<ref>[http://coq.inria.fr/V8.2pl1/contribs/HoareTut.hoarelogicsemantics.html Tutorial on Hoare Logic]: a [[Coq (software)|Coq]] library, giving a simple but formal proof that [[Hoare logic]] is sound and complete with respect to an [[operational semantics]].</ref>
== Beyond predicate transformers ==
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''.
=== Probabilistic Predicate Transformers ===
Line 280 ⟶ 283:
Indeed, such programs have many applications in [[cryptography]] (hiding of information using some randomized noise),
[[distributed systems]] (symmetry breaking).
<ref>{{cite journal |first1=Carroll |last1=Morgan |first2=Annabelle |last2=McIver|author2-link= Annabelle McIver |first3=Karen |last3=Seidel |title=Probabilistic Predicate Transformers |journal=ACM Trans. Program. Lang. Syst. |volume=18 |issue=3 |pages=325–353 |date=May 1996 |doi=10.1145/229542.229547 |url=http://www.cse.unsw.edu.au/~carrollm/probs/Papers/Morgan-96d.pdf |citeseerx=10.1.1.41.9219 |s2cid=5812195 }}</ref>
== See also ==
Line 294 ⟶ 297:
*{{cite book |first=J. W. |last=de Bakker |title=Mathematical theory of program correctness |url=https://archive.org/details/mathematicaltheo0000bakk |url-access=registration |publisher=Prentice-Hall |year=1980 |isbn=978-0-13-562132-5}}
*{{cite journal |first1=Marcello M. |last1=Bonsangue |first2=Joost N. |last2=Kok |title=The weakest precondition calculus: Recursion and duality |journal=[[Formal Aspects of Computing]] |volume=6 |issue=6 |pages=788–800 |date=November 1994 |doi=10.1007/BF01213603 |citeseerx=10.1.1.27.8491 |s2cid=40323488 }}
*{{cite journal |first=Edsger W. |last=Dijkstra |title=Guarded Commands, Nondeterminacy and Formal Derivation of Programs |journal=Comm. ACM |volume=18 |issue=8 |pages=453–7 |date=August 1975 |doi=10.1145/360933.360975 |s2cid=1679242 |doi-access=free }}
*{{cite book |first=Edsger W. |last=Dijkstra |title=A Discipline of Programming |url=https://archive.org/details/disciplineofprog0000dijk |url-access=registration |publisher=Prentice Hall |year=1976 |isbn=978-0-613-92411-5 }} — A systematic introduction to a version of the guarded command language with many worked examples
*{{cite book |first1=Edsger W. |last1=Dijkstra |author2-link=Carel S. Scholten |last2=Scholten |first2=Carel S. |title=Predicate Calculus and Program Semantics |publisher=Springer-Verlag |year=1990 |isbn=978-0-387-96957-2 |series=Texts and Monographs in Computer Science |url=https://books.google.com/books?id=cCbjBwAAQBAJ}} — A more abstract, formal and definitive treatment
| |||