Predicate transformer semantics: Difference between revisions

Revision as of 14:19, 18 July 2016

Revision as of 04:43, 29 September 2016

Line 251:

== Applications ==

* Computations of weakest-preconditions are largely used to statically check [[Assertion (computing)|assertions in programs]] using a theorem-prover (like [[Satisfiabilitysatisfiability Modulomodulo Theoriestheories|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>[[Edsger W. Dijkstra]], ''A constructive approach to program correctness'', BIT Numerical Mathematics, 1968 - Springer</ref> and [[Niklaus Wirth|N. Wirth]].<ref>[[Niklaus Wirth|N. Wirth]], ''Program development by stepwise refinement'', Communications of the ACM, 1971 [http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.90.408&rep=rep1&type=pdf]</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]] library, giving a simple but formal proof that [[Hoare logic]] is sound and complete with respect to an [[operational semantics]].</ref>