
@Article{	  brucker.ea:semantic:2006-b,
  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 programming-like verifications and
		  specification refinement, which are, in our view, necessary
		  to make OCL more fit for future extensions. },
  author	= {Achim D. Brucker and J\"urgen Doser and Burkhart Wolff},
  language	= {USenglish},
  public	= {yes},
  categories	= {holocl},
  classification= {ejournal},
  areas		= {formal methods, software},
  keywords	= {HOL-OCL, UML/OCL, formal semantics},
  title		= {Semantic Issues of {OCL}: Past, Present, and Future},
  editor	= {Birgith Demuth and Dan Chiorean and Martin Gogolla and Jos
		  Warmer},
  issn		= {1863-2122},
  volume	= {5},
  year		= {2006},
  journal	= {Electronic Communications of the EASST},
  copyright	= {ECEASST},
  copyrighturl	= {http://eceasst.cs.tu-berlin.de/index.php/eceasst/article/view/46}
		  ,
  pdf		= {http://www.brucker.ch/bibliography/download/2006/brucker.ea-semantic-2006-b.pdf},
  ps		= {http://www.brucker.ch/bibliography/download/2006/brucker.ea-semantic-2006-b.ps.gz},
  url		= {http://www.brucker.ch/bibliography/abstract/brucker.ea-semantic-2006-b}
		  
}
