Abstract
Although generics became quite popular in mainstream object- oriented languages and several specification languages exist that support the description of generic components, conformance relations between object-oriented programs and formal specifications that have been established so far do not address genericity. In this paper we propose a notion of refinement mapping that allows to define correspondences between parameterized specifications and generic Java classes. Based on such mappings, we put forward a conformance notion useful for the extension of ConGu, a tool-based approach we have been developing to support runtime conformance checking of Java programs against algebraic specifications, so that it becomes applicable to a more comprehensive range of situations, namely those that appear in the context of a typical Algorithms and Data Structures course.
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
Antoy, S., Gannon, J.: Using term rewriting to verify software. IEEE Transactions on Software Engineering 4(20), 259–274 (1994)
Antoy, S., Hamlet, R.: Automatically checking an implementation against its formal specification. IEEE Transactions on Software Engineering 26(1), 55–69 (2000)
Aspinall, D., Sannella, D.: From specifications to code in CASL. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 1–14. Springer, Heidelberg (2002)
Barnett, M., Schulte, W.: Spying on components: A runtime verification technique. In: Proc. Workshop on Specification and Verification of Component-Based Systems 2001 (2001)
Barnett, M., Schulte, W.: Runtime verification of.NET contracts. Journal of Systems and Software 65(3), 199–208 (2003)
Bidoit, M., Mosses, P.: CASL User Manual. LNCS, vol. 2900. Springer, Heidelberg (2004)
Bidoit, M., Sannella, D., Tarlecki, A.: Architectural specifications in CASL. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 341–357. Springer, Heidelberg (1998)
Chen, F., Rosu, G.: Java-MOP: A monitoring oriented programming environment for Java. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 546–550. Springer, Heidelberg (2005)
Chen, F., Tillmann, N., Schulte, W.: Discovering specifications. Technical Report MSR-TR-2005–146, Microsoft Research (2005)
Contract based system development, http://gloss.di.fc.ul.pt/congu/
Edwards, S., Shakir, G., Sitaraman, M., Weide, B., Hollingsworth, J.: A framework for detecting interface violations in component-based software. In: Proc. International Conference on Software Reuse (ICSR) 1998, pp. 46–55 (1998)
Henkel, J., Reichenbach, C., Diwan, A.: Discovering documentation for Java container classes. IEEE Transactions on Software Engineering 33(8), 526–543 (2007)
Leavens, G., Cheon, Y.: Design by contract with JML (2006), http://www.eecs.ucf.edu/~leavens/JML/jmldbc.pdf
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. Science of Computer Programming 55(1–3), 185–208 (2005)
Machado, P.L., Sannella, D.: Unit testing for CASL architectural specifications. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 506–518. Springer, Heidelberg (2002)
Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall PTR, Englewood Cliffs (1997)
Meyer, B.: Eiffel as a framework for verification. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 301–307. Springer, Heidelberg (2008)
Nikolik, B., Hamlet, D.: Practical ultra-reliability for abstract data types. Software Testing, Verification and Reliability 17(3), 183–203 (2007)
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)
Nunes, I., Lopes, A., Vasconcelos, V.T., Abreu, J., Reis, L.S.: Checking the conformance of Java classes against algebraic specifications. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 494–513. Springer, Heidelberg (2006)
Stenzel, K., Grandy, H., Reif, W.: Verification of java programs with generics. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 315–329. Springer, Heidelberg (2008)
Yu, B., King, L., Zhu, H., Zhou, B.: Testing Java components based on algebraic specifications. In: Proc. International Conference on Software Testing, Verification and Validation, pp. 190–198. IEEE, Los Alamitos (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nunes, I., Lopes, A., Vasconcelos, V.T. (2009). Bridging the Gap between Algebraic Specification and Object-Oriented Generic Programming. In: Bensalem, S., Peled, D.A. (eds) Runtime Verification. RV 2009. Lecture Notes in Computer Science, vol 5779. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04694-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-04694-0_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04693-3
Online ISBN: 978-3-642-04694-0
eBook Packages: Computer ScienceComputer Science (R0)