3 Comparison

Most work on library design (e.g., [MS96,Knu93]) follows the traditional style of informal or stylized descriptions and reference implementations. The industrial-strength example of a contract-based library design we know of is Meyer's work [Mey94]. There is, however, some more research work, e. g. the RESOLVE project [SW94]. Both [JC93] and [MMM94] use formal specifications to determine a subsumption relation between components and structure their libraries accordingly. Similarly, [LW94] define the notion of behavioral subtype as an extended means to organize class libraries and [Lea91] has developed techniques to support the specification and verification of object-oriented programs.

Deductive component retrieval has also been investigated by [RW91] which used $\lambda$Prolog to specify the components and its built-in higher-order unification as retrieval mechanism. Moorman Zaremski and Wing [MW95] were the first to explore different match relations; our own work (cf. section 2.2) expands on their results. They also introduced the use of a ``real'' specification language (Larch/ML) for component description. With the exception of [Ste91] which works with algebraic specifications, most other approaches now also use languages which are some sugared variant of first order logic. However, while [MW95] applies the associated interactive LarchProver to solve the proof tasks, their sheer number requires an automated theorem prover as e.g., Otter [MMM94] or SETHEO [FS97] to make it practical.

A more pragmatic approach to deductive retrieval is to use the components types as their specifications (e.g., [Rit91].) This signature matching allows the application of more efficient reasoning mechanisms (e.g., order-sorted theory unification) but also a very concise query formulation. It is thus a successful tool for functional languages which offer rich type structures. The behavioral abstraction which is inherent to types makes an unmodified type-based retrieval unsuited for reuse by contract but it can still be used as a fast pre-filter.

There has also been some earlier work to integrate deductive retrieval into software development environments. The PARIS system [KRT87] supported the semi-automatic construction of programs over a library of so-called schemes, i.e., program fragments which are enriched by assertions about their combination and instantiation possibilites. The construction process then generated proof tasks which were solved by the Boyer-Moore theorem prover. The Inscape system [Per87] aimed at the development of large software systems based on specifications; it also offered some retrieval support. However, both systems worked with severely restricted logics and inference mechanisms and never left the prototype stage.

Lowry et al. [LP⁺94] utilized a formally specified library which contains functions for celestial mechanics and spaceship course computations. After providing a formal specification of e.g. a space vehicle's destination point and time, the system automatically composes a program consisting of calls to appropriate library routines, which compute the flight data. Lowry's system uses a domain-specific logic, which in turn is hidden from the user by a sophisticated graphical user interface.