Simple equational specifications

Abstract

A specification is a description of a signature and a class of algebras over that signature. This amounts to a characterisation of a class of programs, each of which is regarded as a correct realisation of the specification. The fundamental specification technique used in work on algebraic specification, and the one that will be studied in this chapter, is to describe the functional behaviour of the algebras in the class by listing the properties (axioms) they are to satisfy. The simplest and most common case is when these properties are expressed as universally quantified equations. In most of this chapter, we restrict attention to this case, and present basic concepts and results of equational logic. Section 2.7 indicates other forms of ax- ioms that may be of use, along with some possible variations on the definitions of Chapter 1.