High-Precision Retrieval for High-Quality Software
B. Fischer, M. Kievernagel and W. Struckmann
Abteilung f?ur Softwaretechnologie
D-38092 Braunschweig, Germany
Tel. +49 531 3917579
Fax +49 531 3918111
Abstract. 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.
Formal methods are often believed to be the one true way" towards the construction of high-quality software. Their application, however, is surrounded by some myths (Hall, 1990; Bowen and Hinchey, 1995) and industrial usage of formal methods does not live up the initial expectations (Bowen and Stavridou, 1993; Craigen et al., 1993; Weber-Wulff, 1993; Hussmann, 1995). Hence, high-quality software remains an exception.
This unpleasant situation may be overcome or moderated if approved (i. e. specified or even verified) software components can be reused. But then adapting the retrieved components to the exact needs of the user remains an error-prone