Hidden Algebra

Behavioural specification and proof for systems with state


Algebraic techniques have been very successful in specifying and reasoning about data types. Hidden algebra extends these techniques to systems with state, and aims to provide a semantics for software engineering, and for the object paradigm in particular, supporting correctness proofs that are as simple and mechanical as possible. Hidden algebra also aims to provide a simple and intuitive basis for documenting the intended behaviour of software systems.

The hidden algebra approach takes as basic the notion of behavioural abstraction, or more precisely, behavioural satisfaction: this means that specifications characterise how objects (and systems) behave, not how they are implemented. In particular, behavioural abstraction allows more freedom to choose representations in implementations and refinements.

Models of hidden specifications can be thought of as abstract machines that implement the specified behaviour. Behavioural satisfaction of equations means that the left and right sides of the equations denote states that cannot be distinguished by their outputs. In this sense, hidden algebra is an algebraic treatment of abstract automata.

Hidden algebra uses sorts in two distinct ways:

In a sense, these two uses of sorts are dual: induction can be used to establish properties of data types, whereas coinduction establishes properties of objects with state.

Correctness proofs in hidden algebra show that one hidden theory behaviourally satisfies another, and therefore show correctness of behavioural refinements. A standard example of this, the implementation of stacks by arrays and pointers, has an elegant coinductive proof. Larger examples, such as the correctness of an optimising compiler, have also been done in hidden algebra (see the Bibliography page below).



Back to my home page.
Grant Malcolm
Last modified: Mon Jul 31 15:55:49 BST 2006