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.)
|
| Tests are evaluated in a similar way:
|
| 6. The 'truth value' [!s!, B] of test B in normal state !s!
| is defined inductively as follows.
|
| Basis step.
|
| [!s!, T] = T,
|
| [!s!, F] = F.
|
| [!s!, D = E] is _|_ if either [!s!, D] or [!s!, E] is _|_
|
| else is T or F accordingly as [!s!, D] = [!s!, E] or [!s!, D] =/= [!s!, E].
|
| [!s!, D =/= E], [!s!, D < E], [!s!, D =< E], [!s!, D > E], [!s!, D >= E]
|
| are defined similarly.
|
| Inductive step.
|
| Let ~ (not), v (or), & (and) have their usual meanings on the Boolean
| truth values T, F (T for "true", F for "false") so that, for example,
| ~T = F, ~F = T, F & T = F, and so on. Then:
|
| [!s!, (~B)] is _|_ if [!s!, B] is _|_ else is ~[!s!, B].
|
| [!s!, (B v C)] is _|_ if either of [!s!, B] or [!s!, C] is _|_
|
| else is [!s!, B] v [!s!, C].
|
| [!s!, (B & C)] is _|_ if either of [!s!, B] or [!s!, C] is _|_
|
| else is [!s!, B] & [!s!, C].
|
| Manes & Arbib, AAPS, page 8.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤