In this chapter we give a general treatment of structured declarations. This allows us to give an account of language constructs such as structs in C-like languages and objects in object-oriented languages.

In Section 9.2, we describe a big-step semantics of Bur. Then, in Section 9.3, we consider Coat, a small object-oriented language with classes and dynamically generated objects.

Records

In this chapter, we will use the term record to stand for a structured declaration. We shall allow record declarations inside records. Moreover, records may contain both variables and procedures; this is in contrast to languages such as C and Pascal that allow only the declaration of variables in structured declarations. By allowing procedure declarations as part of a record, we can now view a record as an object. Variables then correspond to the local variables of an object and procedures correspond to object methods. Later, in Section 9.3, we extend this understanding so that we can speak of objects that are dynamically generated instances of classes.

In Figure 9.1 we see an example of a program that has nested record declarations. The program consists of a block which has a record r1 that contains the declaration of a variable x, a procedure p and a record r2. The record r2 contains the declaration of two variables, y and z.

In this chapter we encounter our first examples of structural operational semantics, namely big-step and small-step semantics of arithmetic and Boolean expressions. These examples are on a small scale, but they still manage to introduce the principles that we shall be using throughout the remainder of the book.

A structural operational semantics is syntax-directed, and for this reason we first introduce the notion of abstract syntax. We use abstract syntax in this chapter to introduce the language Bims, which forms the core of almost all of the tiny programming languages considered in this book.

The rest of the chapter is devoted to introducing the basics of structural operational semantics. A central concept is that of a transition system. Transition systems are defined using transition rules.

The final section of the chapter briefly explores how we may now formulate and prove properties of a structural operational semantics. We shall return to this topic in later chapters.

Abstract syntax

In order to describe the behaviour of programs we must first present an account of the structure of programs, that is, their syntax. In program semantics we are not interested in syntax analysis – that is part of the theory of parsing. Instead, we are interested in a notion of abstract syntax that will allow us to describe the essential structure of a program. In other words, abstract syntax is not concerned with operator precedence etc.

This chapter gives a short introduction to the general principles of denotational semantics. We do this by giving a denotational semantics of Bims. It turns out that the semantics of while-loops poses a problem, as the obvious semantics is not compositional. However, at the end of the chapter we find a way to circumvent this problem of non-compositionality.

Background

Denotational semantics is a child of the 1960s and is based on the ground-breaking insights of Christopher Strachey and Dana Scott (Strachey, 1966, 1967; Scott and Strachey, 1971). Since then, a lot of work has gone into providing denotational semantics for existing programming languages such as Algol 60, Pascal, Smalltalk and Lisp.

Denotational semantics has also turned out to be a particularly useful tool in the design and implementation of languages such as Ada, CHILL and Lucid (Schmidt, 1986).

Denotational semantics can also be useful in static program analysis, which is the study of the correctness properties on the basis of analyses of the program text (as opposed to analyses of the behaviour of the program).

Simple examples of static analysis involve methods for code optimization. Here are two examples.

Consider the so-called constant-folding problem: when is it possible to replace an expression involving variables by a constant?

In Chapter 5 we saw how one can describe parallel programs using structural operational semantics. Concurrenct behaviour is explained as the nondeterministic interleaving of the steps of the individual parallel components, so to describe this we employ a small-step semantics.

However, the language constructs considered in Chapter 5 allowed parallel components to communicate only by reading and modifying the values of shared variables. In this chapter we take a look at other paradigms for communication between concurrent processes.

The first language that we shall consider in Section 8.1 is very reminiscent of the process calculi CSP (Hoare, 1988) and CCS (Milner, 1989). The languages considered in later sections are all variants of this language.

Section 8.5 of the chapter is devoted to a short introduction to the area of behavioural equivalences for concurrent processes, and in particular to the notion of bisimulation.

CSP and CCS are early examples of process calculi, and the idea of bisimulation equivalence has become prominent here. A process calculus is a simple notation designed with the aim of being able to describe and reason about the behaviour of concurrent processes. The last section of the chapter describes a more recent and very important process calculus which has given rise to a large body of research. This process calculus, the π-calculus, is an expressive yet simple process calculus that allows one to describe phenomena such as references and the transfer of reference.