×

Algebraic approaches to program semantics. (English) Zbl 0599.68008

Texts and Monographs in Computer Science. The AKM Series in Theoretical Computer Science. New York etc.: Springer-Verlag. XIII, 351 p. DM 128.00 (1986).
Programs are syntactic (formal) constructs, written according to well- defined rules, viz. specified by a formal grammar (usually even context- free, except for some details). We want them to mean something, i.e. to define a semantics (e.g. a function of the input vector of values). This has been a real problem in Computer Science, since its inception. The most obvious approach is to keep track of the successive changes that the instructions of a given program operate on the state vector (a so-called computation-sequence), getting finally (if the program does halt) the output vector. This is called the operational semantics.
Interesting though it is, this approach is too ’down-to-earth’, so that people soon felt the need for more abstract (mathematical) semantics. There are at this time three abstract semantics: 1. Assertion semantics due to work by Floyd, Hoare and Wirth that, given a specification of which assertions on the input guarantees that the results satisfy some assertions on the output, constructs a proof that the program satisfies indeed its specification. 2. Denotational semantics due to work by Strachey and Scott. 3. Partially additive semantics due to the authors. This formalizes essentially chaining, conditionals and loops.
The book under review contains three parts: Part 1, Denotational semantics of control, introduces - one chapter at a time - each of the above-mentioned semantics, motivated by analysis of a fragment of Pascal, of a functional programming fragment and of nondeterministic semantics, together with a chapter looking at the bare bones of category theory.
Part 2, Semantics of recursion, is where things really get going: Chapter 5, Recursive specifications, is about the way recursive specification, ever-present in modern programming languages, functions. Chapter 6, Order semantics of recursion, Chapter 7, Canonical fixed points, Chapter 8, Partially additive semantics of recursion and Chapter 9, Fixed points in metric spaces explore the abstract setting behind the theory presented in Chapter 5 in order to be able to extend it to more general semantic categories of Pfn or Mfn, i.e. those partial or multivalued functions.
Part 3, Data types, extends the theory to data types, using the machinery provided by the category theoretical setting. Chapters 10 and 11 introduce functors, fixed points of functors and continuous and co- continuous functors. Chapter 12, Parametric specification, analyzes arrays, stacks, queues and the functional programming fragment of chapter 1. Chapter 13 describes the Order semantics of data types. Chapter 14, Equational specification, introduces the description of data types using operations cum equations and extends functorial fixed points to this area, very much à la mode these last few years.
There have been books written on assertion semantics and denotational semantics respectively. However the book under review is both much wider in breadth (including the former two as well as partially additive semantics) and deeper, using the most general setting - that of category theory - and including a remarkable account of most of the worthwhile papers written in the subject these last few years. It also contains an account of the notions of category theory used, introduced as the need arises. As usual in books co-authored by Arbib in the AKM series, the book is very well written and thus quite easily accessible to beginning graduate students or lower, with many exercises as well as notes and references at the end of each chapter. There is a detailed Author Index and Subject Index, although surprisingly there is no general list of references at the end of the book and no Notation Index either (maybe we have been spoilt by the other volumes in the series). The authors have given us a remarkable book that we should all, teachers and students, be grateful for.
Reviewer: M.Eytan

MSC:

68-02 Research exposition (monographs, survey articles) pertaining to computer science
68Q99 Theory of computing
68Q60 Specification and verification (program logics, model checking, etc.)
18A99 General theory of categories and functors