Semantic Models

Abstract

In his monograph [6], Dana Scott introduces us to a mathematical theory of computation. All values participating in computation, he says, are to be regarded as elements of certain structures called domains. and the existence of these domains in appropriate circumstances is guaranteed by the theory. All this mathematics provides firm foundations on which we may rely when we face the job of specifying the computations we wish to have performed: the theory means that we can be sure we know what we are talking about. In this Chapter we shall consider how these new insights may be exploited in the particular context of the specification of programming languages, by the technique known as Denotational Semantics. We indicate how three important features of conventional languages are handled — assignment, declarations and scopes, and sequencing and jumps — and at each stage we take the opportunity to exhibit a complete definition of “the language so far”, even though each definition will require considerably reworking to accommodate the next stage.

The “denotational semantics” approach to the modelling of programming language concepts: the store and assignment; scopes and environments; continuations and sequencing. Connections with methodologies for correctness of programs and of implementations.