@Article{	  brucker.ea:semantics:2009,
  author	= {Achim D. Brucker and Burkhart Wolff},
  title		= {Semantics, Calculi, and Analysis for Object-oriented
		  Specifications},
  journal	= {Acta Informatica},
  classification= {journal},
  areas		= {formal methods, software},
  keywords	= {UML, OCL, object-oriented specification, refinement,
		  formal methods},
  abstract	= {We present a formal semantics for an object-oriented
		  specification language. The formal semantics is presented
		  as a conservative shallow embedding in Isabelle/HOL and the
		  language is oriented towards OCL formulae in the context of
		  UML class diagrams. On this basis, we formally derive
		  several equational and tableaux calculi, which form the
		  basis of an integrated proof environment including
		  automatic proof support and support for the analysis of
		  this type of specifications.
		  
		  We show applications of our proof environment to data
		  refinement based on an adapted standard refinement notion.
		  Thus, we provide an integrated formal method for
		  refinement-based object-oriented development.},
  year		= {2009},
  language	= {USenglish},
  public	= {yes},
  issn		= {0001-5903},
  doi		= {10.1007/s00236-009-0093-8},
  categories	= {holocl},
  pages		= {255--284},
  month		= jul,
  volume	= {46},
  number	= {4},
  publisher	= {Springer-Verlag},
  address	= {Heidelberg},
  pdf		= {http://www.brucker.ch/bibliography/download/2009/brucker.ea-semantics-2009.pdf},
  url		= {http://www.brucker.ch/bibliography/abstract/brucker.ea-semantics-2009}
		  
}