Content deleted Content added
Line 66:
* Unlike many other semantic formalisms, predicate transformer semantics was not designed as an investigation into foundations of computation. Rather, it is intended to provide programmers with a methodology to develop their programs as "correct by construction" in an "calculation style". This style was advocated by Dijkstra and others, and also developed further in a [[Higher-order_logic|higher order logic]] setting by [[Ralph-Johan Back|R.-J. Back]] in the [[Refinement Calculus]]. It has been mechanized in [[B-Method]].
* Computations of weakest-preconditions are 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]].
* In the meta-theory of [[Hoare logic]], weakest-preconditions are a key notion in the proof of [[ Gödel's_completeness_theorem | relative completness]].
| |||