Abstract:

HOL-OCL: Experiences, Consequences and Design Choices

Achim D. Brucker and Burkhart Wolff


Based on experiences gained from an embedding of the Object Constraint Language (OCL) in higher-order 
logic~citebrucker.ea:proposal:2002, we explore several key issues of the design of a formal semantics of the 
OCL. These issues comprise the question of the interpretation of invariants, pre- and postconditions, their 
transformation, an executable sub-language and the possibilities of refinement notions. A particular emphasize 
is put on the issue of mechanized deduction in UML/OCL specification.