Until relatively recently, rules of algebra followed from assumptions about the unknown quantities, assuming that the symbols represented numerical values for example. By the 20th century, this had been replaced by a more abstract view. The rules could be interpreted in a concrete context if required, but this is not necessary or even appropriate in all circumstances. Other mathematical objects may also be manipulation algebraically and computer programs themselves may be considered as such objects, if assigned a suitable mathematical semantics.
General algebraic laws of programming, applicable to many imperative
programming languages, or subsets of them, have been proposed by
researchers led by
Prof. Tony Hoare
(
knighted
in the year 2000 New Year Honours list),
who took over the leadership of the
Programming Research Group at
Oxford
in 1977 [6]. Many special
purpose process algebras have been proposed, with sets of laws
for their manipulation to enable
formal
reasoning about them. Perhaps the most widely used of these are
Robin Milner's
CCS and Hoare's
CSP
(Communicating Sequential Processes), both useful for reasoning about
concurrent systems. The latter
has inspired the development of the parallel programming language
Occam.
The laws for this language,
developed by
Bill Roscoe,
Hoare and others [10],
have been used to successfully verify the floating-point unit for the
Inmos T800
Transputer,
which has resulted in commercial success for
Inmos Ltd
and prestige in the form of a
Queen's Award for
Technological Achievement.
More
recent work has investigated the
use of algebraic laws in the verification of compiler specifications
[4], either compiling directly
into object code for a machine defined by an interpreter in the
high-level language being compiled, or via a normal form
consisting of a very restricted subset of the high-level language that
is close to the final implementation. The proofs may be mechanised by
systems such as
OBJ, designed by
Prof. Joseph Goguen, at
Oxford 1988-1996, who undertook
much of the theoretical underpinning in the area of initial algebras
and order sorted algebra. This tool facilitates the algebraic
manipulation of mathematical structures (such as programs), with
semi-automation of some of the more mundane aspects including
associative and commutative (``AC'') matching.
Modelling is an important aspect of computer science. However many algebraic properties may be derived from models. To quote Hoare [5]:
A model of a computational paradigm starts with choice of a carrier set of potential direct or indirect observations that can be made of a computational process. A particular process is modelled as the subset of observations to which it can give rise. Process composition is modelled by relating observations of a composite process to those of its components. Indirect observations play an essential role is such compositions. Algebraic properties of the composition operators are derived with the aid of the simple theory of sets and relations.
The viability of such approaches has yet to be seen in widespread industrial practice. As Hoare says [5]:
The construction of a single mathematical model obeying an elegant set of algebraic laws is a significant intellectual achievement; so is the formulation of a set of algebraic laws characterising an interesting and useful set of models.
But neither of these achievements is enough. We need to build up a large collection of models and algebras, covering a wide range of computational paradigms, appropriate for implementation either in hardware or in software, either of the present day or of some possible future.
However the prospects for the use of algebraic techniques in the design and verification of computer based systems are promising if the techniques can become as familiar to engineers as school algebra is to many today.
Jonathan Bowen