Programming Research Group Technical Monograph PRG-114

G Malcolm and J A Goguen

November 1994, 41 pages

The notions of state and observable behaviour are fundamental to many areas of computer science. Hidden sorted algebra, an extension of many sorted algebra, captures these notions through hidden sorts and the behavioural satisfaction of equations. This makes it a powerful formalisation of abstract machines, and many results suggest that it is also suitable for the semantics of the object paradigm. Another extension of many sorted algebra, namely order sorted algebra, has proved useful in system specification and prototyping because of the way it handles subtypes and errors. The combination of these two algebraic approaches, hidden order sorted algebra, has also been proposed as a foundation for object paradigm, and has much promise as a foundation for Software Engineering.

This paper extends recent work on hidden order sorted algebra by investigating the refinement and implementation of hidden order sorted specifications. We present definitions of refinement and implementation for such specifications, and techniques for proving that one specification refines or implements another. It is important that the notions of refinement and implementation be tractable, in the sense that there are efficient techniques for proving their correctness. The proof techniques given in this paper lead, we believe, to correctness proofs that are much simpler than others in the literature. We found that proving refinement is an effective way to prove implementation correctness. Some examples are given.

Any foundation for the semantics of programming should also support modular specifications. The "institutions" developed by Goguen and Burstall are useful for this purpose. Institutions formalise the notion of logical system, and provide an encapsulation property for specifications: when one specification is imported into another, properties that hold of that specification in isolation remain true in its new context. An important technical result of this paper is that hidden order sorted algebra forms an institution, and therefore supports the modular specification of systems of objects. The paper also includes an exposition of hidden order sorted algebra, and brief introductions to many sorted algebra, order sorted algebra, and institutions.