Content deleted Content added
links to guarded commands in wp section |
|||
Line 8:
=== Definition ===
Given
function mapping any [[postcondition]] ''R'' (''R'' denotes thus a predicate on the space of states) to a [[precondition]]. Actually, the result of this function, denoted <math>wp(S, R)</math>, is the "weakest" precondition on the initial state ensuring that execution of ''S'' terminates in a final state satisfying ''R''. More formally, a given ''Hoare triple'' <math>\{ P \} S \{ Q \}</math> is provable in [[ Hoare logic ]] for '''total correctness''' iff the first-order predicate below is universally valid (e.g. for all possible values of the space of states):
:<math>P \Rightarrow wp(S,Q)</math>
Formally, weakest-preconditions are defined recursively over the [[abstract syntax]] of statements. Actually, weakest-precondition semantics is a [[Continuation-passing style]] semantics of state transformers where the predicate in argument is a continuation.
=== Skip ===
Line 40:
As example:
:<math>wp(x:=x-5;x:=x*2\ ,\ x>20)\ =\ wp(x:=x-5,wp(x:=x*2, x > 20))\ =\ wp(x:=x-5,x*2 > 20)\ =\ (x-5)*2 > 20</math>
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.▼
== Other examples of predicate transformers ==
Line 69 ⟶ 73:
* In the meta-theory of [[Hoare logic]], weakest-preconditions are a key notion in the proof of [[ Gödel's_completeness_theorem | relative completness]].
▲== Links with [[Guarded commands]] ==
▲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.
== See also ==
| |||