Predicate transformer semantics: Difference between revisions

Revision as of 13:11, 14 May 2010

Revision as of 13:47, 14 May 2010

Line 50:

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

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

for any initial state statisfying R. 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 <math>''y</math>'' is fresh.

:<math> sp(x := E, R)\ =\ \exists y, x=E[x \leftarrow y] \wedge R[x \leftarrow y]</math> where <math>y</math> 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>