Predicate transformer semantics: Difference between revisions

Revision as of 16:24, 14 May 2010

Revision as of 16:42, 14 May 2010

Line 61:

Given ''S'' a statement and ''R'' a [[ precondition ]] (a predicate on the initial state), then

<math>sp(S, R)</math> is thetheir '''strongest-postcondition''': it implies any postcondition satisfied by the final state of any execution of S,

for any initial state statisfying R. ForIn exampleother words, ona Hoare triple <math>\{ P \} S \{ Q \}</math> is provable in Hoare logic iff the predicate below assignmentis weuniversally havesatisfiable:

<math>sp(S,P) \Rightarrow Q</math>

Hence, if we denote <math>\vec{x}</math> the set of variables occurring free in predicates ''P'' and ''Q'', and if ''S'' is a statement of state space <math>\vec{x}</math>,

we have the following relation between weakest-preconditions and strongest-preconditions:

<math>(\forall \vec{x}, P \Rightarrow wp(S,Q)) \ \Leftrightarrow\ (\forall \vec{x}, sp(S,P) \Rightarrow Q)</math>

For example, on assignment we have:

<math> sp(x := E, R)\ =\ \exists y, x=E[x \leftarrow y] \wedge R[x \leftarrow y]</math> where ''y'' is fresh.

Above, the logical variable <math>''y</math>'' represents the initial value of variable <math>''x</math>''.

Hence,

:<math> sp(x := x - 5, x > 15)\ =\ \exists y, x = y - 5 \wedge y > 15 \ = \ x > 10</math>