Abstract
Reusable software components need expressive specifications. This paper outlines a rigorous foundation of model − based contracts, a method to equip classes with strong contracts that support accurate design, implementation, and formal verification of reusable components. Model-based contracts conservatively extend the classic Design by Contract approach with a notion of model, which underpins the precise definitions of such concepts as abstract object equivalence and specification completeness. Experiments applying model-based contracts to libraries of data structures suggest that the method enables accurate specification of practical software.
This research has been funded in part by Hasler Stiftung, ManCom project, grant # 2146.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R.: The B-book. Cambridge University Press, Cambridge (1996)
Barnett, M., DeLine, R., Fähndrich, M., Jacobs, B., Leino, K.R.M., Schulte, W., Venter, H.: The Spec# programming system: Challenges and directions. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 144–152. Springer, Heidelberg (2008)
Chalin, P.: Are practitioners writing contracts? In: Rigorous Development of Complex Fault-Tolerant Systems, pp. 100–113 (2006)
Gougen, J.A., Thatcher, J.W., Wagner, E.G.: An initial algebra approach to the specification, correctness, and implementation of abstract data types. In: Current Trends in Programming Methodology, pp. 80–149. Prentice-Hall, Englewood Cliffs (1978)
Guttag, J.V., Horning, J.J.: The algebraic specification of abstract data types. Acta Inf. 10, 27–52 (1978)
Hoare, C.A.R.: Proof of correctness of data representations. Acta Inf. 1, 271–281 (1972)
Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. Sci. Comput. Program. 55(1-3), 185–208 (2005)
Meyer, B.: Object-oriented software construction, 2nd edn. Prentice Hall, Englewood Cliffs (1997)
Meyer, B., Fiva, A., Ciupa, I., Leitner, A., Wei, Y., Stapf, E.: Programs that test themselves. Computer 42(9), 46–55 (2009)
Polikarpova, N., Furia, C.A., Meyer, B.: Specifying reusable components, Extended version, http://arxiv.org/abs/1003.5777
Schoeller, B.: Making classes provable through contracts, models and frames. PhD thesis, ETH Zurich (2007)
Schoeller, B., Widmer, T., Meyer, B.: Making specifications complete through models. In: Architecting Systems with Trustworthy Components, pp. 48–70 (2004)
Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: PLDI 2008, pp. 349–361. ACM, New York (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Polikarpova, N., Furia, C.A., Meyer, B. (2010). Specifying Reusable Components. In: Leavens, G.T., O’Hearn, P., Rajamani, S.K. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2010. Lecture Notes in Computer Science, vol 6217. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15057-9_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-15057-9_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15056-2
Online ISBN: 978-3-642-15057-9
eBook Packages: Computer ScienceComputer Science (R0)