8 Comparison with related work

Back has been an early pioneer of refinement calculus [Bac78] and research in this topic has lead to a textbook [Mor94] and a comprehensive foundation [BvW97]. The calculus has emerged from Dijkstra's seminal work on weakest preconditions and an influential paper by Wirth [Wir71]. A monograph by Dijkstra and Scholten [DS89] approaches the underlying mathematics in an unconventional way and Wim Hesselink discloses more insight in [Hes92]. A predominant quality of refinement calculus is the elaborated interplay of specified and executable code. Different from its origins, Morgan and Back allow miraculous statements [Mor88], which is a source of an ongoing controversy. Miraculous statements are based on the lattice join operation and have no executable interpretation. Therefore, they have been excluded by the healthiness laws [Dij76] in the very beginning.

The basic concept of object-orientedness is subclassing (inheritance). An important reinforcement is behavioral subtyping, which has been introduced e.g. in POOL [Ame90]. Subclassing is code inheritance in its simplest form, where method signatures are compared for type compatibility. A more sophisticated comparison is achieved by the contra/covariance rules. Subtyping goes deeper and a comparison includes, similar to the refinement relation, the semantic behavior of the compared methods. Liskov and Wing have given a precise subtype definition [LW94]. To capture the semantics, they specify class methods in the two tiered style of Larch [GH93]. The subtype definition is high-level and involves method names and signatures.

Refinement calculus identifies programs with the elements of the predicate transformer lattice. The partial order of the lattice, i.e. the refinement order, relates two programs, which are at different abstraction levels. In the development of object-oriented programs, the basic elements are classes rather than programs. An obvious but often unnoticed novelty is that classes at different abstraction levels coexist: abstract and concrete classes. In the Oberon project [WG92], I have experienced how abstract classes are designed by software architects and handed over to developers who elaborate concrete classes. When only the definition without an additional description of the specification and application types is given, however, developers have no means to perform their task. [Szy92] was an exceptional project.

Lattice theory is a well-understood discipline in mathematics [DP90]. Lattices are well suited to formalize models with two parties. This is particularly the case for software user and programming interfaces which can be compared with a contract between two parties [Heu95b]. Guided by the duality of lattices, the notion of an application type is introduced. Application types are expected to play a major rôle in the formal specification of modular software components [DL95].

The draft [Heu97b] presents in a simplified setting a lattice-theoretical approach to the development of object-oriented programs. It introduces a class construct so that classes become elements in the lattice. As for action systems [BS94] and higher constructs in the B method [Abr96], syntactic sugar is added on top of a primitive language based on a primitive language as presented in [BvW97].

In difference to [BvW97], the lattice structure rather than the refinement order is postulated and the interpretation of meets and joins is initially searched for, thereby inverting the interpretation of the refinement order, which coincides with the subtype definition. The lattice order relates classes, which are at different abstraction levels. The inverted interpretation enables the calculation of abstract common superclasses as the join of implementations. This shows that meaning, which is useful in the development of object-oriented programs, can be assigned to the join operation.