the tautology Whereas, the formula reduces to the wrong proposition . 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 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 relative completeness. Beyond predicate transformers Weakest-preconditions and strongest-postconditions of imperative expressions 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 monads. Among them, Hoare Type Theory combines Hoare logic for a Haskell-like language, separation logic and type theory. This system is currently implemented as a Coq library called Ynot. In this language, evaluation of expressions corresponds to computations of strongest-postconditions. Probabilistic Predicate Transformers Probabilistic Predicate Transformers are an extension of predicate transformers for probabilistic programs. Indeed, such programs have many applications in cryptography (hiding of information using some randomized noise), distributed systems (symmetry breaking). See also Axiomatic semantics — includes predicate transformer semantics Dynamic logic — where predicate transformers appear as modalities Formal semantics of programming languages — an overview Notes References — A systematic introduction to a version of the guarded command language with many worked examples — A more abstract, formal and definitive treatment Formal methods Program logic Edsger W. Dijkstra