2.5 Obstacles

There are a couple of problems which make a successful implementation of reuse by contract a hard task. The major impediment is the general acceptance problem of formal methods. As one colleague put it: ``If I need a sort routine, I say grep sort!''

Without a formal software development process, the up-front costs become fairly high. Programmers are not used to contracting and may consider it merely as an additional burden which remains without any benefit as long as there are no or not enough specified libraries to be reused. Library construction, however, is time-consuming and expensive, especially when it is not supported by the feed-back described above. Worst of all, due to the general indifference in formal methods, the market offers only very few specified libraries to begin this process with.

The ``look and feel'' of a reuse system also can impair its usefulness. If the end user has to deal with complicated parameter settings for the prover, specify details he considers irrelevant, or provide postconditions in some cryptic prover language, reuse by contract will not be successful.

Another source of problems is the computational complexity of deductive component retrieval. Long response times due to insufficient deductive power can easily render the entire concept impractical; this in particular affects scale-up for big libraries or complicated components. Contracts for larger components which in turn promise larger pay-offs may become too large or too complicated. A more technical aspect may lead to even more complicated proof tasks. If provider and client use different mathematical concepts (e.g., sets and lists) the resulting ``view mismatch'' can only be solved if the prover deduces the necessary mappings.

In a non-formal software process, the use of formal specifications can even hamper the retrieval abilities. The reason is that recall may suffer from the overwhelming precision of formal specifications. If there is a component which differs only slightly from what the user wants, it will not be found, because the proof obligation can not be fulfilled (``near miss''). Theorem provers do not have a notion of an ``almost provable'' statement, and it is this sharp distinction between true and false statements which may backfire in a reuse context. Note that in a formal process, this problem does not occur as partial or ``fuzzy'' contract fulfillment is not acceptable.