Specifying Reusable Components

Reusable software components need well-defined interfaces, rigorously and completely documented features, and a design amenable both to reuse and to formal 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, implementation, and formal verification of reusable components. Model-based contracts conservatively extend the classic Design by Contract by means of expressive models based on mathematical notions, which underpin the precise definitions of noch as abstract equivalence and specification completeness. Preliminary experiments applying model-based contracts to libraries of data structures demonstrate the versatility of the methodology and suggest that it can introduce rigorous notions, but still intuitive and natural to use in practice.

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: Nadia Polikarpova, Carlo A. Furia, Bertrand Meyer
• Keywords: CORR 2010, Education, Formal Verification, Model-based Contracts, Reusable Software Components