Content deleted Content added
Merge wlp into this article |
m Anchor, remove redundant link, layout |
||
Line 1:
'''Predicate transformer semantics''' is an extension of [[Hoare logic|Floyd-Hoare Logic]] invented by [[Edsger W. Dijkstra|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]] 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 precondition'''" <math>wp(S, R)</math>. Here ''S'' denotes a list of ''commands'' and ''R'' denotes a predicate on the space, called the "[[postcondition]]". 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 assignment statement:
Line 7 ⟶ 8:
This gives a predicate that is a copy of ''R'' with the value of ''x'' replaced by ''E''.
{{Anchor|Weakest liberal precondition}} An important variant of the weakest precondition is the '''weakest liberal precondition''' <math>wlp(S, R)</math>, which yields the weakest condition under which ''S'' either does not terminate or establishes ''R''. It therefore differs from ''wp'' in not guaranteeing termination.
An example of a valid calculation of ''wp'' for assignments with integer valued variables ''x'' and ''y'' is:
Line 14 ⟶ 16:
This means that in order for the "post-condition" ''x > 10'' to be true after the assignment, the "pre-condition" ''y > 15'' must be true before the assignment. This is also the "weakest pre-condition", in that it is the "weakest" restriction on the value of ''y'' which makes ''x > 10'' true after the assignment.
Dijkstra also defined alternative ('''if''') and repetitive ('''do''') constructs as well as a composition operator (''';''') using ''wp''. The alternative and repetitive constructs used ''[[guarded commands]]'' to influence execution. Because of the rules he imposed on the definition of ''wp'', both constructs allow for non-deterministic execution if the ''[[guard (computing)|guard]]s'' in the commands are non disjoint.
Line 25 ⟶ 28:
* [[Formal semantics of programming languages]] — an overview
* [[Hoare logic]] — the best-known axiomatic semantics
== References ==
| |||