Abstract:

Semantic Issues of OCL: Past, Present, and Future

Achim D. Brucker and Jürgen Doser and Burkhart Wolff


We report on the results of a long-term project to formalize the semantics of OCL 2.0 in Higher-order Logic 
(HOL). The ultimate goal of the project is to provide a formalized, machine-checked semantic basis for a theorem 
proving environment for OCL (as an example for an object-oriented specification formalism) which is as faithful 
as possible to the original informal semantics. We report on various (minor) inconsistencies of the OCL s
emantics, discuss the more recent attempt to align the OCL semantics with UML 2.0 and suggest several 
extensions which make, in our view, OCL semantics more fit for future extensions towards programming-like 
verifications and specification refinement, which are, in our view, necessary to make OCL more fit for future 
extensions.