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 assume that the reader already has a good idea of what the semantics of
| our fragment should be. (For example, the algorithm described by (2) always
| terminates with identifier 'a' storing the value 0.) A formal operational
| semantics is as follows.
|
| We imagine an abstract computer with one memory location set aside for each
| identifier. Each location stores a single value, where a 'value' is either a
| natural number or the symbol _|_ meaning "as yet undefined". At any time, only
| finitely many locations store a number. The effect of executing a statement is
| to assign numerical values to identifiers by evaluating numerical expressions
| according to an algorithm controlled by tests and conditional and repetitive
| constructs. (Here we ignore overflow: our numerical operations +, -, *, ÷, for
| addition, subtraction, multiplication, and division compute exact integer values
| no matter how large.) The only thing that can "go wrong" is that we might attempt
| to evaluate an expression containing identifiers for which no numerical values have
| been assigned. When this happens we wish to abort the computation and so we create
| a special 'abort state' !w! [omega]. Every other state is a 'normal state' which we
| define to be a function !s! [sigma] from the set of all identifiers to the set of all
| values, with the requirement that !s!(I) =/= _|_ for only finitely many identifiers I.
| The 'initial state' is the function !t! [tau] which assigns _|_ to each identifier.
|
| The operational semantics of a statement S will be defined as
| a 'computation sequence' of states beginning with the initial
| state !t! and taking one of the forms (4a), (4b), or (4c):
|
| 4a. !t!, !s!_1, ..., !s!_n, !w! (n > 0, all !s!_i =/= !w!);
|
| 4b. !t!, !s!_1, ..., !s!_n, ... (all !s!_i =/= !w!);
|
| 4c. !t!, !s!_1, ..., !s!_n (n >= 0, all !s!_i =/= !w!).
|
| In (4a), 'computation aborts'.
|
| In (4b), 'computation is nonterminating'.
|
| In (4c), the computation 'terminates' in a normal state !s!_n.
|
| Manes & Arbib, AAPS, pages 6-7.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤