Predicate transformer semantics: Difference between revisions

Revision as of 14:00, 22 July 2023

Revision as of 14:08, 22 July 2023

Line 153:

=== Goto statement ===

Formalization of jump statements like ''{{mono|goto}} L'' takes a very long bumpy process. A common belief seems to indicate the goto statement could only be argued operationally. This is probably due to a failure to recognize that ''{{mono|goto}} L'' is actually miraculous (i.e. non-strict) and does not follow Dijkstra's coined Law of Miracle Excluded, as stood in itself. But it enjoys an extremely simple operational view from the weakest precondition perspective, which was unexpected. We define

{| style="background-color:#eeeeff;" border="1" cellpadding="10"

|<math>wp(\texttt{goto}\ L, R) = wpL</math>

where ''wpL'' is the weakest precondition at label ''L''.

|}

For ''{{mono|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 ''{{tmath|wp(L:S, Q )''}} for some ''Q'' computed to that point. 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 ''{{tmath|S(L:L: S1)''}}, which is the same as ''{{tmath|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 }

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

Line 179 ⟶ 180:

post(x ← 0)

Therefore,
wp(S, post ) = post(x ← 0) .

== Other predicate transformers ==