PROVING CORRECTNESS OF REFINEMENT AND IMPLEMENTATION
Joseph A. Goguen, Grant Malcolm · 2009
The notions of state and observable behaviour are fundamental to many areas of computer scjpnce. Hidden sorted algebra, an extension of many sorted al~bra. 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 semanticl:i of the object paradigm. Another extension of many sorted algebra, namely order sorted algebra, hM 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 heen proposed as a foundation for object paradigm. and has mnch promise as a foundation for Software Engineering. This paper extends recent work on hidden order sorted algebra by investigat.ing: tbe re finement and implementation of bidden order sort.ed specificatious. We present definitions of rpfint'ment and implementatiou for such sppcifications, and tl'{:hniques for proving tbat one specification refines or implements another. It is important that the notions of relinement and implementation be tractable, in the sense that there are efficient techniques for proving their correctnpss. The proof techniques given in this paper lead, we believe, to correctness proofs that are much simpler than others in the literature. \Ve found that proving refinement is an effective way to prove implementation correctness. Some examples are given. AllY foundation for the spmantks of programming should also support modular specifi cations. The 'institutions' developed hy Goguen and Bllrstall are useful for this purpose. Institutions formalise the notion of logical system, and provide an encapsulation property for specifications: when oue specification is imported into another, properties that hold of that specification in isolation remain true in its uew context. An important technical r€Sult of this paper is that hidden order sorted algebra forms au 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.