NORA/HAMMR: Making Deduction-Based Software Component Retrieval Practical

Deduction-based software component retrieval uses preand postconditions as indexes and search keys and an automated theorem prover (ATP) to check whether a component matches. This idea is very simple but the vast number of arising proof tasks makes a practical implementation very hard. We thus pass the components through a chain of filters of increasing deductive power. In this chain, rejection filters based on signature matching and model checking techniques are used to rule out non-matches as early as possible and to prevent the subsequent ATP from “drowning.” Hence, intermediate results of reasonable precision are available at (almost) any time of the retrieval process. The final ATP step then works as a confirmation filter to lift the precision of the answer set. We implemented a chain which runs fully automatically and uses MACE for model checking and the automated prover SETHEO as confirmation filter. We evaluated the system over a medium-sized collection of component...

• Type: Conference
• Year: 1997
• Where: KBSE
• Authors: Johann Schumann, Bernd Fischer 0002
• Keywords: Automated Theorem Prover, KBSE 1997, Model Checking, Retrieval Uses Preand, Software Engineering