Content deleted Content added
m →Strongest postcondition: Dark mode |
|||
| (40 intermediate revisions by 16 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 ===
We use '' T '' to denote the predicate that is everywhere true and '' F '' to denote the one that is everywhere false. We shouldn't at least conceptually confuse ourselves with a Boolean expression defined by some language syntax, which might also contain true and false as
=== Skip ===
{|
|<math>wp(\texttt{skip},R) \ =\ R</math>
|}
=== Abort ===
{|
|<math>wp(\texttt{abort},R) \ =\ \texttt{
|}
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
where ''y'' is a fresh variable and not free in E and R (representing the final value of variable ''x'')
|}
* 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
|}
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 ''INV'', called the [[
{|
|<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>
|}
==== 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}}, <)
{|
|<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
\begin{array}[t]{l}
Z: [Z\equiv(E\wedge wp(S, Z)) \vee (\neg E \wedge R)]
Line 117 ⟶ 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 144 ⟶ 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 150 ⟶ 152:
|}
It combines Morgan's syntactic idea with the sharpness idea by Bijlsma, Matthews and Wiltink.<ref>Chen, Wei and Udding, Jan Tijmen, "The Specification Statement Refined" WUCS-89-37 (1989).
https://openscholarship.wustl.edu/cse_research/749</ref>
=== Goto statement ===
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''.
|}
For ''{{mono|goto}} L'' execution transfers control to label ''L'' at which the weakest precondition has to hold.
The way that ''wpL'' is referred to in the rule should not be taken as a big surprise. It is just
wp(do x > 0 → L: x := x-1 od; if x < 0 → x := -x; goto L ⫿ x ≥ 0 → skip fi, post)
= { sequential composition and alternation rules }
wp(do x > 0 → L: x := x-1 od, (x<0 ∧ wp(x := -x; goto L, post)) ∨ (x ≥ 0 ∧ post)
Line 169 ⟶ 172:
wp(do x > 0 → L: x := x-1 od, x<0 ∧ wpL(x ← -x) ∨ x≥0 ∧ post)
= { repetition rule }
the strongest solution of
Z: [ Z ≡ x > 0 ∧ wp(L: x := x-1, Z) ∨ x < 0 ∧ wpL(x ← -x) ∨ x=0 ∧ post ] = { assignment rule, found wpL = Z(x ← x-1) }
the strongest solution of
Z: [ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← x-1) (x ← -x) ∨ x=0 ∧ post] = { substitution }
the strongest solution of
Z:[ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← -x-1) ∨ x=0 ∧ post ] = { solve the equation by approximation }
post(x ← 0)
Therefore,
wp( == Other predicate transformers ==
Line 194 ⟶ 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 204 ⟶ 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 222 ⟶ 229:
=== Strict ===
A predicate transformer ''S'' is '''strict''' iff:
:<math>
For instance, ''wp'' is artificially made strict, whereas ''wlp'' is generally not. In particular, if statement ''S'' may not terminate then
<math>wlp(S,\texttt{
:<math>wlp(\texttt{while}\ \texttt{true}\ \texttt{do}\ \texttt{skip}\ \texttt{done}, \texttt{
Indeed, '''
The non-strict but monotonic or conjunctive predicate transformers are called miraculous and can also be used to define a class of programming constructs
https://openscholarship.wustl.edu/cse_research/671</ref>
=== Terminating ===
A predicate transformer ''
:<math>
Actually, this terminology makes sense only for strict predicate transformers: indeed, <math>wp(S,\texttt{
It seems that naming this property '''non-aborting''' would be more appropriate: in total correctness, non-termination is abortion, whereas in partial correctness, it is not.
=== Conjunctive ===
A predicate transformer ''
:<math>
This is the case for <math>wp(S,.)</math>, even if statement ''S'' is non-deterministic as a selection statement or a specification statement.
=== Disjunctive ===
A predicate transformer ''
:<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 259 ⟶ 266:
Whereas, the formula <math>wp(S, x=0) \vee wp(S,x=1)</math>
reduces to the ''wrong proposition'' <math>(0=0 \wedge 1=0) \vee (1=0 \wedge 1=1)</math>.
== Applications ==
* 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 272 ⟶ 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 279 ⟶ 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 293 ⟶ 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
| |||