Abstract
The paradigm of design by contract provides a transparent way of specifying object-oriented systems. There exist a number of languages for contractual specification including OCL, JML and Spec#. Nevertheless, there are still a number of research problems concerning this approach. One of them is the implementation of primitive @pre in OCL or equivalently old in JML. Those primitives are used in post-conditions to refer to attribute values in states preceding an operation execution. There are a number of implementations of this operators, but all suffer logical and computational problems. In this paper, existing approaches to the implementation of @pre are discussed and a new solution is proposed.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
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)
Briand, L., Dzidek, W., Labiche, Y.: Using Aspect-Oriented Programming to Instrument OCL Contracts in Java, Tech. Rep. SCE-04-03, Carleton Univ. (2004)
Darvas, A., Müller, P.: Reasoning About Method Calls in JML Specifications. In: Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs (FTfJP 2005), Glasgow, Scotland (July 2005)
DOT, Dresdener OCL Toolkit, http://dresden-ocl.sourceforge.net/
Dzidek, W., Briand, L., Labiche, Y.: Lessons Learned from Developing a Dynamic OCL Constraint Enforcement Tool for Java. In: Bruel, J.-M. (ed.) MoDELS 2005. LNCS, vol. 3844, pp. 10–19. Springer, Heidelberg (2006)
Floyd, R.W.: Assigning meanings to programs, in Mathematical Aspects of Computer Science. In: Proceedings of Symposium in Applied Mathematics, vol. 19, pp. 19–32. American Mathematical Society (1967)
Hussmann, H., Finger, F., Wiebicke, R.: Using Previous Property Values in OCL Postconditions: An Implementation Perspective. In: Int. Workshop UML 2.0 - The Future of the UML Constraint Language OCL, York, UK, October (2000)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns. Addison- Wesley, Reading (1995)
Hoare, T.: An Axiomatic Basis for Computer Programming. CACMÂ 12(10) (1969)
Karaorman, M., Abercrombie, P.: jContractor: Introducing Design-by-Contract to Java Using Reflective Bytecode Instrumentation. Formal Methods in System Design 27(3), 275–312 (2005)
Laddad, R.: AspectJ in Action: Practical Aspect-Oriented Programming, Manning (2003)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J.: JML Reference Manual, Tech. Rep. 2007/02/07, Iowa State Univ. (2007)
Meyer, B.: Applying design by contract. Computer 25(10), 40–51 (1992)
Meyer, B.: Eiffel: The Language. Object- Oriented Series. Prentice Hall, New York (1992)
OMG, OCL 2.0 Specification, Version 2005-06-06 (June 2005)
Richters, M., Gogolla, M.: Aspect-Oriented Monitoring of UML and OCL Constraints. In: Proc. UML 2003 Workshop on Aspect-Oriented Software Development with UML. Illinois Institute of Technology, Department of Computer Science (2003)
Toval, A., Requena, V., Fernandez, J.: Emerging OCL Tools. Journal of Software and System Modelling 2(4), 248–261 (2003)
Van Der Straeten, R., Casanova, R.: Stirred but not Shaken: Applying Constraints in Object-Oriented Systems. In: Proc. of NetObjectDays, pp. 138–150 (2001)
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
Kosiuczenko, P. (2009). On the Implementation of @pre. In: Chechik, M., Wirsing, M. (eds) Fundamental Approaches to Software Engineering. FASE 2009. Lecture Notes in Computer Science, vol 5503. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00593-0_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-00593-0_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00592-3
Online ISBN: 978-3-642-00593-0
eBook Packages: Computer ScienceComputer Science (R0)