Foundations of Algebraic Specification and Formal Program Development

Don Sannella and Andrzej Tarlecki

Contents:

Preface.

0. Introduction.

This chapter provides the basic motivations which underlie the later technical material, by presenting our view of the role of specifications in program development. This is to allow us to avoid most discussion of directly practical motivations in the technical chapters which follow.

1. Universal algebra.

This chapter is intended as a minimally-explained summary of what a computer scientist needs to know about universal algebra.

2. Simple equational specifications.

This chapter summarizes the traditional approach to algebraic specification with some ideas concerning ways in which the definitions may be altered.

3. Category theory.

This chapter is intended as a minimally-explained summary of what a computer scientist needs to know about basic category theory. Uses material in Chapters 1 and 2 as examples. Provides a few examples which will be used later.

4. Working within an arbitrary logical system.

This chapter introduces institutions as a formalisation of the intuitive notion of a logical system. This provides a framework to present the technical material of the remaining chapters at an appropriate level of generality.

5. Structured specifications.

This chapter presents an ASL-style kernel specification formalism comprising a number of simple but powerful specification-building operations. The material is institution independent but the presentation will make constant reference to particular institutions.

6. Parameterisation.

This chapter discusses: parameterised specifications, parameterised programs, and specifications of parameterised programs, extending to higher-order. Motivation: another dimension for generalisation is to make things generic (in the sense of schematic).

7. Formal program development.

This chapter presents a framework for formal program development by stepwise refinement of specifications. Each implementation step involves a construction which, whenever given a model of the implementing specification, yields a model of the implemented specification.

8. Behavioural specifications

In this chapter we introduce the fundamental concept of behavioural equivalence and discuss its role in software specification and development.

9. Proofs for specifications

In this chapter we examine the proof-theoretic counterparts of the semantic notions introduced in earlier chapters.

10. The category of institutions.

This chapter presents some more advanced topics in the theory of institutions.