4 Research Topics

Although specified component libraries are a necessary requirement for any code reuse mechanism working with formal methods and not only for reuse by contract, they are a nearly extinct species. We think that the community should take up the lead of Meyer and work towards realistic, formally specified libraries which must also cover non-functional aspects of components which traditionally matter for the users, e. g. structure sharing. This work should also include the development of appropriate domain-specific logics.

Larger benefits are expected from reusing components of a much coarser granularity than simple functions (``megaprogramming'', [WWC92].) Scaling-up specification methods to such megacomponents requires a lot of further research. First of all, flexible components are parameterized (generic packages, C++ templates etc). Thus even signature matching requires higher-order unification. A next step could be an investigation about specifications of design patterns or parameterized modules/functors. Having a fully specified pattern library would be a nice argument.

Scale-up also concerns deductive retrieval. First of all, the provers must be adapted to reflect a situation where there are thousands of simple proof obligations, and almost all of them are non-theorems. Furthermore, methods have to be developed for fast rejection of non-theorems which do not compromise recall. One promising candidate is abstract model checking [Jac94]. Probably the combination of behavioural subtyping and signature matching also works to this end.

Finally, to increase the number of reuse opportunites, the strict compatibilities defined in 2.2 could by relaxed by introducing some approximate reasoning. However, this requires appropriate automatic component adaption mechanisms to maintain the integrity of reuse by contract.