A Proposal for a Formal OCL Semantics in Isabelle/HOL

Abstract 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.

• Type: Conference
• Year: 2002
• Where: TPHOL
• Authors: Achim D. Brucker, Burkhart Wolff
• Keywords: Automated Reasoning, Conservative Shallow Embedding, Object Constraint Language, Open Standardization Process, TPHOL 2002