Applications
- Computations of weakest-preconditions are largely used to statically check assertions in programs using a theorem-prover (like SMT-solvers or proof assistants): see Frama-C or 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 and N. Wirth. It has been formalized further by R.-J. Back and others in the Refinement Calculus. Some tools like B-Method provide now 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 relative completness.
Read more about this topic: Predicate Transformer Semantics