VCR: A VDM-based software component retrieval tool

We present a tool which allows implicit VDM specifications to be used as search keys for the retrieval of software components. A preprocessing phase utilizes signature matching to filter promising candidates out of a component library. The actual specification matching phase builds proof obligations from the specifications of key and candidates and feeds them into a theorem prover. Validated obligations denote matching components. First experiments clearly demonstrate the feasibility of this approach. We thus get a high-precision retrieval tool which helps programmers in locating components which exactly match their needs.