Content deleted Content added
m Disambiguating links to Coq (link changed to Coq (software); link changed to Coq (software); link changed to Coq (software)) using DisamAssist. |
|||
Line 267:
* 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 274:
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=http://ynot.cs.harvard.edu/papers/jfpsep07.pdf }}</ref>
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 ===
| |||