@Article{	  brucker.ea:semantic:2007,
  abstract	= {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
		  semantics, 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 program verifications and specification
		  refinement.},
  author	= {Achim D. Brucker and J\"urgen Doser and Burkhart Wolff},
  journal	= {Electronic Communications of the EASST},
  language	= {USenglish},
  pdf		= {papers/2007/easst-glitches.pdf},
  title		= {Semantic Issues of {OCL}: Past, Present, and Future},
  volume	= 5,
  year		= 2007,
  user		= {doserj}
}