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 (cont.)
|
| Before discussing assertion semantics we must first introduce assertions.
| An 'assertion' is a statement about the program state which is either true
| or false. As an example, consider the (hopefully transparent) program 1.
|
| 1. INPUTS: X
| OUTPUTS: Y
| {X >= 0}
| BEGIN
| (a block of code representing
| an algorithm for Y := X^½ )
| END
| {X = Y * Y}.
|
| The assertions are shown enclosed by braces, "{" and "}". They are not
| part of the program, but assert what properties 'should' hold true when
| the assertion is encountered in executing the program. A program is
| 'correct' if indeed the satisfaction of all initial assertions about
| the input data guarantees the truth of all assertions encountered
| later on.
|
| One could attempt to design a programming language with assertions in mind.
| All built-in functions would come with associated assertions and for each
| programming construct there would be rules explaining how to find suitable
| assertions for the overall construct from the pieces of the construct and
| their assertions. Ideally, every program would automatically be strewn
| with assertions with the following beneficial effects. The assertions
| would usefully document the program, and it would be possible to write
| software that could automatically scan the assertions to detect bugs
| and check for correctness.
|
| In the next section we introduce a small fragment of Pascal giving a
| formal syntax and an operational semantics. In Section 1.3, however, we
| introduce a functional programming fragment that makes no use of identifiers
| or assignment statements. Here, the concept of "state" (which in Section 1.2
| means the values stored by the identifiers) would require major overhaul before
| one could give an operational semantics or an assertion semantics. It is hard
| to create general semantic theories devoid of built-in assumptions about the
| programming languages to which they apply!
|
| Manes & Arbib, AAPS, pages 4-5.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤