ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| Algebraic Approaches to Program Semantics
|
| Part 1. Denotational Semantics of Control
|
| Chapter 1. An Introduction to Denotational Semantics
|
| 1.1. Syntax and Semantics
|
| To specify a programming language we must specify its syntax and semantics.
| The 'syntax' of a programming language specifies which strings of symbols
| constitute valid programs. A formal description of the syntax typically
| involves a precise specification of the alphabet of allowable symbols
| and a finite set of rules delineating how symbols may be grouped into
| expressions, instructions, and programs. Most compilers for programming
| languages are implemented with 'syntax checking' whereby the first stage
| in compiling a program is to check its text to see if it is syntactically
| valid. In practice, syntax must be described at two levels, for a human
| user through programming manuals and as a syntax-checking algorithm within
| a compiler or interpreter.
|
| "Semantics" is a technical word for "meaning". A 'semantics' for
| a programming language explains what programs in that language mean.
| In more mathematical terms, semantics is a function whose input is a
| syntactically valid program and whose output is a description of the
| function computed by the program.
|
| There are different approaches to semantics. We briefly introduce three:
| operational semantics, denotational semantics, and assertion semantics.
| We will give an example of an operational semantics in the next section.
| Assertion semantics will be further considered in Chapter 4. Denotational
| semantics is a major concern of this book.
|
| Manes & Arbib, AAPS, pages 1-3.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤