Book Chapter: Deduction-Based Software Component Retrieval

We present an application of automated theorem proving to software engineering: the reuse of software components based on their formal specifications. Such specifications can be viewed as contracts. Our work is motivated by the fact that safe reuse can only be achieved in a contract-based development process, where contracts are used as the actual medium for component retrieval. Theorem provers can be applied to match contracts against user queries, thus retrieval becomes a deduction problem. This application presents some unique challenges because a huge amount of proof tasks is generated, most of them being non-theorems. In order to achieve acceptable response time, our retrieval system NORA/HAMMR uses an incremental filter pipeline. Components are first selected or rejected by signature matching and model checking; the prover is only applied to components which survived earlier stages in the pipeline. This chapter describes design and underlying technology of NORA/HAMMR. It concludes with several empirical evaluations of retrieval performance in connection with the provers PROTEIN, SETHEO and SPASS.