2.6 Possible Solutions

There is no medicine for people who reject formal methods. The only argument which might appeal to them is that reuse by contract is not going to replace existing, established retrieval methods, but to augment them. For all the other problems, solutions can be outlined as follows.

First of all, a retrieval system based on formal specifications must hide the deductive machinery completely. Any details for setting prover parameters, synchronizing parallel-running provers, generating prover input etc. must be invisible to the user. Instead, the retrieval tool should offer an interface which utilizes the end user's language and concepts; in particular, it should also offer access to more traditional retrieval algorithms. As somebody has to take care of preprocessing and tuning the formal specifications and tune the deductive engine, we propose that this is done by an expert. The end user must not be bothered by this.

In order to tackle the performance and scale-up problems, we utilize two mechanisms: abstraction and incrementality. Abstraction means that not always a traditional formal specification will be needed, somtimes a more compact component description is sufficient. Multiple layers of specifications can be used to separate the core functionality from non-functional implementation aspects as e. g. structure sharing [PH95]. This can be achieved by a domain-specific logic which would not only improve the deductive abilites of the system but would also be beneficial for the end user.

Incrementality means that several processes must cooperate in order to achieve an increasing reduction of the problem space. NORA/HAMMR uses a filter chain in order to reduce the burden of the theorem prover. The chain consists of a series of filters of increasing power, the prover is only the last element in the chain. Chain configuration may vary; a typical filter chain includes signature matching and model checking. Signature matching selects components according to a specification of their interface alone. Model checking is used in order to discover non-theorems: if a counterexample in some small model can be found, the proof obligation is considered a non-theorem and the component rejected. Both techniques may negatively affect recall as well as precision, as a counterexample in a finite model of, say, the integers may be invalid, and demanding identical interfaces is too restrictive. But they greatly reduce the burden of the prover, as only a small number of proof obligations survives the preliminary filters.

Signature matching can also help with the view mismatch problem. It identifies the structural similarities between the types in question which in turn can be used to construct some of the abstraction functions automatically.

In order to reduce the risc of not finding components due to overspecification or ``near misses'' of the prover, we again propose abstraction and incrementality. The user interface must allow to incrementally sharpen the postcondition (or weaken the precondition), thereby incrementally filtering the set of surviving components. Furthermore, use of a domain-specific specification language offers the appropriate abstractions to the user; near misses due to erroneous low-level specification details are avoided.