1 Background

Reuse by contract is the application of formal methods to software reuse: software components are associated with contracts--formal models of their functional behaviour--and administered, retrieved, and reused by these.

Similar approaches have been proposed before (e.g., [KRT87,RW91,MM91]) but without convincing success. The goal of our project NORA/HAMMR[FKS95c,FKS95b,FKS95a] is thus to make reuse by contract practical . We investigate

• scalable and efficient architectures for reuse by contract,
• reuse-friendly specification techniques,
• library organization techniques based on contracts,
• deductive component retrieval,
• its interaction with formal software development processes, and
• the integration of reuse by contract and conventional reuse mechanisms.

Our long-term goal is to build a system which smoothly integrates component design, implementation, and verification with the systematic reuse of a fully specified and verified component library.

Our work on NORA/HAMMR started in 1994. Our main topic so far has been the application of automated deduction techniques to solve the proof tasks emerging from deductive component retrieval. A large number of experiments done in collaboration with colleagues from the German joint research project on deduction show that current theorem provers are capable to solve enough of the emerging tasks. Our implementation is tailored towards these experiments. It uses VDM as contract language but can generate proof tasks for different theorem provers. We currently work on an improved library organziation and the integration of a program verification system.