Using Patterns to Map OCL Constraints to JML Specifications

OCL is a formal notation to specify constraints on UML models that cannot otherwise be expressed using diagrammatic notations such as class diagrams. The type of constraints that can be expressed using OCL include class invariants and operation preconditions and post-conditions. Constraint patterns can be used to simplify the development of consistent constraints for UML/OCL models. This paper investigates an approach based on constraint patterns to developing JML specifications for Java implementations from OCL constraints. This would enable the checking of OCL constraints at runtime since they can be translated to JML executable assertions. The approach involves mapping each OCL constraint pattern to a corresponding JML pattern. This results in a library of JML constraint patterns that provides a seamless transition from UML/OCL designs to Java implementations.