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.)
|
| The principal semantic definition is:
|
| For any normal state !s! the 'computation sequence' of S starting at !s!
| is a state sequence <!s!, S> of one of the three forms (8a), (8b), (8c):
|
| 8a. !s!, !s!_1, ..., !s!_n, !w! (n >= 0, all !s!_i =/= !w!);
|
| 8b. !s!, !s!_1, ..., !s!_n, ... (all !s!_i =/= !w!);
|
| 8c. !s!, !s!_1, ..., !s!_n (n >= 0, all !s!_i =/= !w!).
|
| (with interpretations similar to those of (4a), (4b), (4c))
| defined inductively as follows.
|
| 9. Basis step.
|
| ( !s!, !w! if [!s!, E] = _|_
| <!s!, I := E> = <
| ( !s!, !s!_1 else,
|
| where
|
| ( !s!(J) if J =/= I
| !s!_1(J) = <
| ( [!s!, E] if J = I.
|
| This is the expected meaning. Identifier I is assigned the
| value obtained by evaluating E, as long as this is possible,
| and other identifiers are left unchanged.
|
| Inductive step.
|
| 10. Composition.
|
| Define
|
| <!s!, begin end> = !s!
|
| and define
|
| <!s!, begin S_1 end> = <!s!, S_1>.
|
| Proceeding inductively on the number of statements, assume that
|
| <!s!, begin S_2; ...; S_k+1 end>
|
| has been defined for every normal state !s!
| and every k statements S_2, ..., S_k+1.
|
| Then
|
| <!s!, begin S_1; ...; S_k+1 end>
|
| is defined as follows.
|
| It is defined to be
|
| <!s!, S_1>
|
| if "S_1 fails to terminate normally starting at !s!", that is,
| if <!s!, S_1> has one of the forms (8a), (8b). Otherwise,
|
| <!s!, S_1> = !s!, !s!_1, ..., !s!_n
|
| as in (8c), so we define
|
| <!s!, begin S_1; ...; S_k+1 end>
|
| to be the sequence
|
| !s!, !s!_1, ..., !s!_n-1, <!s!_n, begin S_2; ...; S_k+1 end>.
|
| In short, we form the sequence obtained if each S_i+1 begins where the
| previous S_i leaves off, save that this cannot continue if computation
| aborts or one of the S_i did not terminate.
|
| 11. Conditional.
|
| ( <!s!, !w!> if [!s!, B] = _|_
| <!s!, (if B then R else S)> = < <!s!, R > if [!s!, B] = T
| ( <!s!, S > if [!s!, B] = F
|
| Repetitive constructs.
|
| The computation sequence <!s!, (while B do S)> is given by (12).
|
| 12. While-do statement.
|
| ( !s!, !w! if [!s!, B] = _|_
| <!s!, (while B do S)> = <
| ( !s! if [!s!, B] = F
|
| <!s!, (while B do S)> = <!s!, S> if [!s!, B] = T
| and <!s!, S> has one
| of the forms (8a, 8b).
|
| <!s!, (while B do S)> = !s!, !s!_1, ..., !s!_n-1, <!s!_n, (while B do S)>
|
| if [!s!, B] = T
| and <!s!, S> has the form
| !s!, !s!_1, ..., !s!_n of (8c).
|
| This sequence may, of course, fail to terminate.
| We leave it to the reader to formulate a similar
| definition for <!s!, (repeat S until B)>.
|
| 13. The 'computation sequence' <S> of the statement S is <!t!, S>,
| where !t! is the initial state mapping each identifier to _|_.
| The operational semantics of our Pascal fragment is complete.
|
| Manes & Arbib, AAPS, pages 9-11.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤