ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| Algebraic Approaches to Program Semantics
|
| Part 1. Denotational Semantics of Control
|
| Chapter 1. An Introduction to Denotational Semantics
|
|
| 1.2. A Simple Fragment of Pascal (cont.)
|
| We now turn to the details of how to associate a definite sequence of
| states to a statement. Here the description of Table 1 provides a guide.
| (We substitute the more mathematical terms "basis step" for "given outright"
| and "inductive step" for "building rules" from now on.) We must first assign
| appropriate values to expressions and tests (a process that depends on the state).
|
| 5. The 'value' [!s!, E] of expression E in normal state !s!
| is defined inductively as follows.
|
| Basis step.
|
| If E is a numeral, [!s!, E] is the
| usual base-10 natural number value
| of E (with leading zeros ignored).
|
| If E is an identifier, [!s!, E] = !s!(E).
|
| Inductive step.
|
| If either [!s!, D] = _|_ or [!s!, E] = _|_ then
|
| [!s!, (D+E)] = [!s!, (D-E)] = [!s!, (D*E)] = [!s!, (D÷E)] = _|_.
|
| Else
|
| [!s!, (D + E)] = [!s!, D] + [!s!, E]
|
| [!s!, (D - E)] = [!s!, D] -°- [!s!, E]
|
| [!s!, (D * E)] = [!s!, D] · [!s!, E]
|
| [!s!, (D ÷ E)] = [!s!, D] div [!s!, E]
|
| are the expected natural-number arithmetic operations
| so that x -°- y means the maximum of 0 and x - y, and
| x div y is the largest integer =< y/x, that is, the
| unique integer q with y = qx + r, where the remainder
| r satisfies 0 =< r < x.
|
| (Here we have relied on the earlier-stated fact that there
| is only one way to decouple an expression; if there were
| more than one way the above rules might assign values to
| expressions ambiguously.)
|
| To illustrate how (5) is used, suppose that !s!(a) = 3. Then:
|
| [!s!, ((a + 5) * 2)]
|
| = [!s!, (a + 5)] · [!s!, 2]
|
| = ([!s!, a] + [!s!, 5]) · [!s!, 2]
|
| = (3 + 5)(2)
|
| = 16
|
| Manes & Arbib, AAPS, pages 7-8.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤