Introduction to Algebraic Specification
There are several different forms for formal specification. Algebraic specification, or property based specification, differs from model based specification systems such as Z, or VDM) in the degree of abstraction. Algebraic specification seeks to defer implementation decisions as much as possible, seeking to determine all possible models that fulfill the requirements. The theory of algebraic specification is grounded in universal algebra, category theory, and logic. This level of abstraction makes algebraic specification a powerful way of analysing system requirements. Algebraic Foundations
Algebraic specification operates in terms of an abstract mathematical construction called many sorted universal algebras. There is a lot of powerful mathematical theory behind such objects, but for the purposes of this introduction we can think of it as a set of typed objects, along with a set of typed functions mapping sequences of objects to a single result object. From the programmers point of view this means that every object (term) in the algebra is a possible state of the program, and more importantly every possible state of the program can be explicitly expressed as an object or term from the algebra. For those with some background in modern algebra, the usual constructions of sub-algebras, ideals, and quotient algebras all transfer naturally, along with canonical versions of homomorphisms, kernels, and the isomorphism theorems - that is to say, such algebras behave nicely and are well understood mathematically. This is all well and good, but what is required is a representation for such an algebra that is both compact and comprehensible. Given such a representation it would then be possible to use the mathematics to fully analyse the behaviour of any program that implemented the types and functions described by the algebra. Again abstract mathematics comes to our aid: we can describe the algebra in terms of a many sorted signature, a set of base terms, and axioms defining properties of the operations in terms of the base terms (this should be familiar to anyone who has seen presentations of groups). Remembering that a a many sorted algebra is made up of typed objects, and functions on those objects, a many sorted signature is simply a set of type names, and a set of named type signatures for functions. Axioms are simply equations (at the most basic level just using first order equational logic) that restrict the behaviour of the operations named in the signature. A (many sorted algebra) presentation is then a many sorted signature and associated axioms. Given such a presentation we can then ask what algebras (concrete implementations) satisfy the axioms. Given a loose enough specification there may be many algebras that satisfy the presentation - this is known as the class of models of the presentation. We can also ask, given a class of algebras with a fixed signature, for the presentation given by the set of axioms that all those algebras satisfy - this is known as the theory of the class. Finally we can talk about the closure of a presentation - the theory of the class of models of the presentation. A closed presentation is one which is equal to its closure. A signature may include operations that take no parameters (a 0-ary operator) and simply return a result. The resulting terms in the algebra generated by such operations are called ground terms as they are necessarily present in all algebras with the given signature. Given a model of a presentation, we say that the model has junk if it contains elements that cannot be generated solely from ground terms, and we say the model has confusion if theory of the model contains axioms not in the presentation. A model is called initial if it contains neither junk nor confusion. The important result is that initial models are unique up to isomorphism - that is all implementations of the initial model of presentation are guaranteed to be functionally equivalent. Given a specification in the form of a presentation, we can determine a unique algebra with no junk or confusion that satisfies it. If we can codify a set of requirements into a signature and set of axioms, we can completely define a mathematical object (that brings to bear all of the powerful mathematical machinery of modern abstract algebra) that completely describes the state space of software implementing those requirements. For now this sounds very abstract and theoretical, but by casting things in such abstract mathematical form we gain a great deal of flexibility, as well as a powerful mathematical tool-set that has already been developed with which to analyse, prove, and verify specifications.