High-Precision Retrieval for High-Quality Software

In this paper we present VCR, a high-precision retrieval tool which helps programmers to locate software components which exactly match their needs. It employs implicit VDM specifications as search keys and is thus especially well-suited for a formal software development process based on VDM's specify-refine-implement paradigm. VCR is designed as a filter-inspector-chain which is user-configurable through a graphical user interface. The filters realize deduction-based search methods such as signature matchers, model checkers, and theorem provers. The inspectors maintain links between subsequent filters and thus allow examination and reuse of intermediate retrieval results. First experiments demonstrate the feasibility of our approach.