Conference Papers: SETHEO Goes Software Engineering: Application of ATP to Software Reuse

[fischer97cade]Bernd Fischer, Johann Schumann, SETHEO Goes Software Engineering: Application of ATP to Software Reuse, Proceedings of the 14th International Conference on Automated Deduction, pp. 65--68, Townsville, July 1997.


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.




Authors at the institute

Former Staff Member
Prof. Dr. rer. nat. Bernd Fischer