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
|
| In this section we describe an abbreviated version of Pascal.
| Although this limited version has full computing power with
| regard to functions whose inputs and outputs are natural
| numbers, this is a tangential point -- the main objective
| of this section is to illustrate how to present a formal
| syntax as well as an operational semantics for a simple
| programming language. The reader should observe that
| the level of precision of the operational semantics
| is such that it becomes fairly clear how to write
| a compiler or interpreter for the Pascal fragment,
| so that we accomplish more than an exercise in
| formalizing what we already knew.
|
| The complete syntax of our Pascal fragment is given in Table 1.
|
| Table 1. The Syntax of a Pascal Fragment
| ---------------------------------------------------
|
| 'Alphabet of Symbols'
|
| Digits: 0, 1, ..., 9
|
| Letters: a, b, ..., z
|
| Parentheses: ( , )
|
| Boolean Truth Values: T, F
|
| Boolean Connectives: ~, v, &
|
| Comparisons: =, =/=, <, =<, >, >=
|
| Arithmetic Functions: +, -, *, ÷
|
| Statement Constructors:
|
| :=, ;, begin, end, if, then, else, while, do, repeat, until
|
| The set of 'expressions' is defined by:
|
| Given Outright:
|
| Any nonempty string of digits (called a 'numeral'),
| a letter followed by a (possibly empty) string of
| digits and letters (called an 'identifier').
|
| Building Rules:
|
| If D, E are expressions
| so are (D + E), (D - E), (D * E), (D ÷ E).
|
| The set of 'tests' is defined by:
|
| Given Outright:
|
| T, F,
|
| D = E, D =/= E, D < E, D =< E, D > E, D >= E,
| for any two expressions D, E.
|
| Building Rules:
|
| If B, C are tests so are (~B), (B v C), (B & C).
|
| The set of 'statements' is defined by:
|
| Given Outright:
|
| I := E, if I is an identifier and E is an expression.
|
| Building Rules:
|
| If S_1, ..., S_n are statements (n >= 0), so is:
|
| begin S_1; ...; S_n end.
|
| If B is a test and R, S are statements, so are:
|
| (if B then R else S),
|
| (while B do S),
|
| (repeat S until B).
|
| ---------------------------------------------------
|
| Here, the colons, commas, and periods are 'not' among the 64 symbols
| in the alphabet. Parentheses are used liberally to ensure that there
| is exactly one way to derive an expression, test, or statement using
| the building rules and beginning with those which are given outright.
| We do not give a formal proof of this here, but encourage the reader
| to explore this (see Exercise 1). Three examples of expressions are:
|
| ((a + 5) * 2),
|
| 572,
|
| (cat + (dog + mouse)),
|
| whereas, according to our rules,
|
| a + 5
|
| is not an expression. An example of a statement is shown in (2).
|
| 2. begin a := 5; (while (a > 0 & a =/= 6) do a := a - 1) end
|
| Note that begin, while, do, and end are single symbols
| in the chosen alphabet and that there is no space symbol
| in the alphabet. Normally, one displays a statement so as
| to be more readable by humans, for example, as in (3).
|
| 3. begin
| a := 5;
| (while (a > 0 & a =/= 6) do a := a - 1)
| end
|
| This is harmless since we obtain (2) from (3) by ignoring the
| aspects (in this case the vertical arrangement and the spaces)
| which are not expressible in the formal syntax.
|
| Manes & Arbib, AAPS, pages 5-6.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
Nota Bene. In this transcription, I found it too distracting
to mark the syntactic keywords in bold -- as #begin# or #end# --
by way of attempting to emulate the authors' practice in mine,
so I must ask for my reader's indulgence in the way of making
intelligent adjustments, 'mutatis mutandis', in the reception.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤