Konferenzartikel: Deduction-Based Software Component Retrieval

We present a retrieval approach which allows pre- and postconditions of software components to be used as search keys. A component qualifies, if it has a weaker precondition and a stronger postcondition than the search key. In contrast to previous work, our tool NORA/HAMMR allows for configurable chains of deduction-based filters such as signature matchers, model checkers --- which will be our main subject here ---, and resolution provers; the latter can be run with dynamically adjusted axiom sets and inference rules. Hence, instead of feeding the search key and all components' specifications to a theorem prover in a batch-like fashion, NORA/HAMMR allows for incremental narrowing of the search space along the filter chain, and interactive inspection of intermediate results.