Translating the Object Constraint Language into the Java Modelling Language

ABSTRACT

The Object Constraint Language OCL is a textual specification language that could be used for constraining the modelling elements that occur in UML diagrams. Typical constraints include class invariants and preconditions and postconditions of operations. The Java Modelling Language (JML) is a behavioural interface specification language designed for specifying Java classes and interfaces. This paper defines a translation of OCL expressions and constraints into the Java Modelling Language. The objective of this translation is to be able to map UML object-oriented designs with OCL constraints to Java classes and interfaces annotated with JML specifications, and to carry out logical reasoning about such classes and interfaces using JML tools which include a run time assertion checker and an interactive prover based on PVS.

REFERENCES

• 1: Ken Arnold , James Gosling, The Java programming language (2nd ed.), ACM Press/Addison-Wesley Publishing Co., New York, NY, 1998
• 2: Alex Borgida , John Mylopoulos , Raymond Reiter, On the Frame Problem in Procedure Specifications, IEEE Transactions on Software Engineering, v.21 n.10, p.785-798, October 1995 [doi>10.1109/32.469460]
• 3: Cheon, Y. and Leavens, G., A Runtime Assertion Checker for the Java Modeling Language (JML). In Software Engineering Research and Practice (SERP'02), pages 322--328. CSREA Press, June 2002.
• 4: John V. Guttag , James J. Horning, Larch: languages and tools for formal specification, Springer-Verlag New York, Inc., New York, NY, 1993
• 5: Cliff B. Jones, Systematic software development using VDM (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 6: Leavens G., Baker A., and Ruby C., JML: A notation for detailed design. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds, editors, Behavioral Specifications of Businesses and Systems, pages 175--188. Kluwer Academic Publishers, Boston, 1999.
• 7: Leavens G., Baker A., and Ruby C., Preliminary Design of JML: A Behavioral Interface Specification Language for Java. TR98-06, revised version 2003.
• 8: Gary T. Leavens , Clyde Ruby , K. Rustan , M. Leino , Erik Poll , Bart Jacobs, JML (poster session): notations and tools supporting detailed design in Java, Addendum to the 2000 proceedings of the conference on Object-oriented programming, systems, languages, and applications (Addendum), p.105-106, January 2000, Minneapolis, Minnesota, United States [doi>10.1145/367845.367996]
• 9: Bertrand Meyer, Eiffel: the language, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• 10: Rational Software Corporation. The Object Constraint Language Specification Version 2.0. Available at http://www.rational.com, 2003.
• 11: Rational Software Corporation. The Unified Modeling Language UML Version 2.0. Available at http://www.rational.com, 2003.
• 12: James Rumbaugh , Ivar Jacobson , Grady Booch, The Unified Modeling Language reference manual, Addison-Wesley Longman Ltd., Essex, UK, 1998
• 13: J. M. Spivey, The Z notation: a reference manual, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1992
• 14: Jos Warmer , Anneke Kleppe, The object constraint language: precise modeling with UML, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1998

INDEX TERMS

Keywords:
JML, OCL, UML, constraints, reasoning