Predicate transformer semantics: Difference between revisions

Revision as of 10:53, 29 November 2022

Revision as of 10:57, 29 November 2022

Line 163:

For ''goto L'' execution transfers control to label ''L'' at which the weakest precondition has to hold.

The way that ''wpL'' is referred to in the rule should not be taken as a big surprise. It is just ''wp(S(L:S1), post)''. This is like any wp rules, using constituent statements to give wp definitions, even though ''goto L'' appears a primitive. The rule does not require the uniqueness for locations where ''wpL'' holds within a program, so theoretically it allows the same label to appear in multiple locations as long as the weakest precondition at each ___location is the same wpL. The goto statement can jump to any of such locations. This actually justifies that we could place the same labels at the same ___location multiple times, as ''S(L:L: S1)'', which is the same as ''S(L: S1)''. Also, it does not imply any scoping rule, thus allowing a jump into a loop body, for example. Let us calculate wp of the following program, which has a jump into the loop body.

'' wp(do x > 0 → L: x := x-1 od; if x < 0 → x := -x; goto L ⫿ x ≥ 0 → skip fi, post)''

= { sequential composition and alternation rules }

'' wp(do x > 0 \rightarrow→ L: x := x-1 od, (x<0 \wedge∧ wp(x := -x; goto L, post)) \vee∨ (x ≥ 0 ∧ post)

''wp(do x > 0 \rightarrow L: x := x-1 od, (x<0 \wedge wp(x := -x; goto L, post)) \vee

(x >= 0 \wedge post)''

= { sequential composition, goto, assignment rules }