Content deleted Content added
Line 162:
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 S, 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 }
Line 169:
wp(do x > 0 → L: x := x-1 od, x<0 ∧ wpL(x ← -x) ∨ x≥0 ∧ post)
= { repetition rule }
the strongest solution of
Z: [ Z ≡ x > 0 ∧ wp(L: x := x-1, Z) ∨ x < 0 ∧ wpL(x ← -x) ∨ x=0 ∧ post ] = { assignment rule, found wpL = Z(x ← x-1) }
the strongest solution of
Z: [ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← x-1) (x ← -x) ∨ x=0 ∧ post] = { substitution }
the strongest solution of
Z:[ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← -x-1) ∨ x=0 ∧ post ] = { solve the equation by approximation }
post(x ← 0)
Therefore, wp(
== Other predicate transformers ==
| |||