Abstract:

A Proposal for a Formal OCL Semantics in Isabelle/HOL

Achim D. Brucker and Burkhart Wolff


We present a formal semantics as a conservative shallow embedding of the Object Constraint Language (OCL). 
OCL is currently under development within an open standardization process within the OMG; our work is an 
attempt to accompany this process by a proposal solving open questions in a consistent way and exploring 
alternatives of the language design. Moreover, our encoding gives the foundation for tool supported reasoning 
over OCL specifications, for example as basis for test case generation.