Specifying reusable components

Reusable software components need well-defined interfaces, rigorously and completely documented features, and a design amenable both to reuse and to for-mal verification; all these requirements call for expressive specifications. This paper outlines a rigorous foundation to model-based contracts, a methodology to equip classes with expressive contracts supporting the accurate design, implemen-tation, and formal verification of reusable components. Model-based contracts conservatively extend the classic Design by Contract by means of expressive mod-els based on mathematical notions, which underpin the precise definitions of no-tions such as abstract equivalence and specification completeness. Preliminary experiments applying model-based contracts to libraries of data structures demon-strate the versatility of the methodology and suggest that it can introduce rigorous notions, but still intuitive and natural to use in practice.