SETHEO Goes Software Engineering: Application of ATP to Software Reuse

Reuse of approved software components has been identified as one of the key factors for successful software engineering projects. Although the reuse process also covers many non-technical aspects we will restrict ourselves to the retrieval of software components (SCR) based on their formal specifications. Our system NORA/HAMMR is based on a library of software components with associated specifications of their pre- and postconditions written in VDM-SL. A query consists of pre- and postconditions pre_q, post_q and the signature of the desired component. Plug-in-compatibility of a library component c is guaranteed, if (pre_q => pre_c) \& (post_c => post_q) can be shown. This "retrieval-by-proof'' or deduction-based approach to SCR has been proposed before but without convincing success. These earlier failures result from the strong application requirements, like critical ("sub-minute'') response times and full automatic processing: the proof tasks must be generated and processed completely automatically as we cannot expect the end-user to cope with ATP details.