2.4 Benefits

For the users, the biggest visible benefit is of course the ability to retrieve components which provably match their needs. Provably matching components increase the overall quality of the software. They also improve the software process, the productivity and other aspects of software development. Depending on the kind of compatibility used (plug-in, conditional or partial), several benefits can be identified.

Plug-in compatibility - and, to a smaller extent, conditional compatibility - are most useful in a formal development process. Here, it can be used for the safe composition of components. A component which satisfies a proof task is guaranteed not to compromise the overall correctness. This is true even for conditional compatibility, if - as is often the case - the refinement process can generate the component's precondition. Safe composition prevents reuse disasters like the Ariane case. Safe composition is a must for any safety-critical software project which wants to utilize component reuse, and reuse by contract is the only available technology.

In some cases software composition from formally specified components can be done automatically. By means of constructive type theory, a formal specification can be transformed into executable code which may also contain calls to (formally specified) library components. Needless to say, the resulting code is provably correct.

Once a new piece of software has been constructed by safe composition, automatically or not, it can be added to the library. Hence the basis for reuse is increased, without any additional overhead: in a formal process, the specification of a new component or subsystem must be supplied anyway. Furthermore, reuse by contract offers additional support for a formal development process. Development steps are larger, and an actual implementation for subsystems can be obtained early, thereby supporting vertical prototyping. If new components are added to the library, a positive feedback is obtained which encourages the use of formal specifications and dedicated technology and tools (e.g. verifiers) for a formal development process.

In a less formal software process, reuse by contract still improves software development. In such a context, partial compatibility will be most useful. Partial compatibility has highest recall, but may require manual checks or even component modifications in order to match the components precondition. For a software developer whose primary interest is to find reusable components, this is not an obstacle. If the primary goal is to reuse code, the developer will be ready to provide the stronger precondition needed for conditional compatibility, or even extend the component's functionality in order to utilize partial compatibility. Still, use of a formal postcondition considerably increases the precision of component search, that is, reduces the probability of finding irrelevant components.

Reuse by contract is attractive even for those who prefer commercial success over safety or improved component retrieval. Today's libraries (for example, the Standard Template Library for C++) are not formally specified. If different vendors offer the same library, there will be subtle differences between implementations. As a consequence, a user will not be able to switch from one library implementation to another - enabling library monopolies and preventing innovative vendors with small market share from commercial success. Hence market transparency requires that there is an implementation-independent specification - a standard - for a component library. Today, such standards have been established in other software and hardware areas; usage of formal specifications as standards for libraries will result in better return on investment for independent library vendors.