Content deleted Content added
No edit summary |
mNo edit summary |
||
Line 1:
'''Predicate transformer semantics''' is an extension of [[Hoare_logic|Floyd-Hoare Logic]] invented by [[Dijkstra]] and extended and refined by other researchers. It was first introduced in Dijkstra's paper "Guarded commands, nondeterminacy and formal derivation of programs". It is a method for defining the semantics of an [[Imperative_programming|imperative programming]] language by assigning to each ''command'' in the language a corresponding ''predicate transformer''. A ''predicate transformer'' is a [[Total function|total function]] mapping between two ''[[assertion (computing)|predicates]]'' on the state space of a program.
The canonical ''predicate transformer'' of sequential imperative programming is the so-called "weakest pre-condition" <math>wp(S, R)</math>. Here ''S'' denotes a list of ''commands'' and ''R'' denotes a predicate on the space, called the "post-condition". The result of applying this function gives the "weakest pre-condition" for ''S'' terminating with ''R'' true. An example is the following definition of the
:<math> wp(x := E, R) = R_E^x </math>
Line 17:
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 a "calculational style". This style was advocated by Dijkstra and others, and also developed further in a [[Higher-order_logic|higher order logic]] setting by R.J Back in the [http://www.ecs.soton.ac.uk/~mjb/refcalc-tut/home.html Refinement Calculus].
Although the most common and most widely discussed because of their relevance to sequential programming, "weakest pre-conditions" are not the only ''predicate transformers''. For example, [[Leslie Lamport]] has suggested ''win'' and ''sin'' as ''predicate transformers'' for [[
== References ==
| |||