Abstract
We present and evaluate an approach for the run-time conformance checking of Java classes against property-driven algebraic specifications. Our proposal consists in determining, at run-time, whether the classes subject to analysis behave as required by the specification. The key idea is to reduce the conformance checking problem to the runtime monitoring of contract-annotated classes, a process supported today by several runtime assertion-checking tools. Our approach comprises a rather conventional specification language, a simple language to map specifications into Java types, and a method to automatically generate monitorable classes from specifications, allowing for a simple, but effective, runtime monitoring of both the specified classes and their clients.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Antoy, S., Hamlet, R.: Automatically checking an implementation against its formal specification. IEEE TOSE 26(1), 55–69 (2000)
Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B.: Algebraic Foundations of Systems Specification. IFIP State-of-the-Art Reports. Springer, Heidelberg (1999)
Barnett, M., Schulte, W.: Spying on components: A runtime verification technique. In: Proc. WSVCBS — OOPSLA 2001 (2001)
Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Bartetzko, D., Fisher, C., Moller, M., Wehrheim, H.: Jass - Java with assertions. ENTCS 55(2) (2001)
Bidoit, M., Mosses, P.: CASL User Manual. LNCS, vol. 2900. Springer, Heidelberg (2004)
Contract based system development, http://labmol.di.fc.ul.pt/congu/
Ehrig, H., Mahr, G. (eds.): Fundamentals of Algebraic Specification 1: Equations and Initial Semantics. Springer, Heidelberg (1985)
Gannon, J., Purtilo, J., Zelkowitz, M.: Software specification: A comparison of formal methods (2001)
Goguen, J., Thatcher, J., Wagner, E.: An initial algebra approach to the specification, correctness, and implementation of abstract data types. In: Current Trends in Programming Methodology. Data Structuring, vol. IV, pp. 80–149. Prentice-Hall, Englewood Cliffs (1978)
Guttag, J., Horning, J., Garland, S., Jones, K., Modet, A., Wing, J.: Larch: Languages and Tools for Formal Specification. Springer, Heidelberg (1993)
Henkel, J., Diwan, A.: Discovering algebraic specifications from java classes. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743. Springer, Heidelberg (2003)
Henkel, J., Diwan, A.: A tool for writing and debugging algebraic specifications. In: Proc. ICSE 2004 (2004)
Huges, M., Stotts, D.: Daistish: Systematic algebraic testing for OO programs in the presence of side-effects. In: Proc. ISSTV, pp. 53–61. ACM Press, New York (1996)
Karaorman, M., Holzle, U., Bruno, J.: jContractor: A reflective Java library to support design by contract. In: Cointe, P. (ed.) Reflection 1999. LNCS, vol. 1616, p. 175. Springer, Heidelberg (1999)
Kramer, R.: iContract - The Java Design by Contract Tool. In: Proc. TOOLS USA 1998. IEEE Computer Society Press, Los Alamitos (1999)
Leavens, G., Leino, K.R.M., Poll, E., Ruby, C., Jacobs, B.: JML: notations and tools supporting detailed design in java. In: OOPSLA 2000 Companion, pp. 105–106. ACM Press, New York (2000)
Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall PTR, Englewood Cliffs (1997)
Nunes, I., Lopes, A., Vasconcelos, V., Abreu, J., Reis, L.: Testing implementations of algebraic specifications with design-by-contract tools. DI/FCUL TR 05–22 (2005)
Spivey, J.: The Z Notation: A Reference Manual. ISCS. Prentice-Hall, Englewood Cliffs (1992)
Man Machine Systems. Design by contract for java using jmsassert. Published on the internet (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nunes, I., Lopes, A., Vasconcelos, V., Abreu, J., Reis, L.S. (2006). Checking the Conformance of Java Classes Against Algebraic Specifications. In: Liu, Z., He, J. (eds) Formal Methods and Software Engineering. ICFEM 2006. Lecture Notes in Computer Science, vol 4260. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11901433_27
Download citation
DOI: https://doi.org/10.1007/11901433_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-47460-9
Online ISBN: 978-3-540-47462-3
eBook Packages: Computer ScienceComputer Science (R0)