PROVING CORRECTNESS OF REFINEMENT AND IMPLEMENTATION

Abstract

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.