KIT | KIT-Bibliothek | Impressum

SETHEO Goes Software Engineering: Application of ATP to Software Reuse

Fischer, Bernd; Schumann, Johann

Abstract: 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.


Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Proceedingsbeitrag
Jahr 1997
Sprache Englisch
Identifikator ISBN: 978-3-540-63104-0
ISSN: 0302-9743
KITopen ID: 1000017602
Erschienen in Automated Deduction - CADE-14. 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13 - 17, 1997. Proceedings. Ed.: W. McCune
Verlag Springer, Berlin
Seiten 65 - 68
Serie Lecture notes in computer science ; 1249
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page