7 Conclusions

  Components need semantic specifications. Black-box specifications, revealing only input-output behavior are not sufficient for interactive components making external calls. White-box specifications require detailed understanding and fix too many details, making alternate implementations and future enhancements impossible. Grey boxes, as a middle ground, reveal the states at which external calls are made and the sequence of calls, while abstracting from implementation details.

Specification languages should be based on the same paradigm and use a similar notation as the implementation language to improve acceptance and reduce transformation difficulties. Tool support for simulation and proving greatly enhances the appeal of specification languages.

Of the surveyed specification approaches, abstract statements best fit the requirements for grey-box specifications and for wide acceptance. The seamless approach between specification and implementation provided by the refinement calculus is an added bonus.

Acknowledgments

We would like to thank the referees for their helpful comments and Ralph Back, Emil Sekerinski, and Clemens Szyperski for a number of fruitful discussions.