@PhDThesis{	  brucker:interactive:2007,
  author	= {Achim D. Brucker},
  title		= {An Interactive Proof Environment for Object-oriented
		  Specifications},
  school	= {ETH Zurich},
  year		= 2007,
  type		= {Ph.D. Thesis},
  month		= mar,
  classification= {thesis},
  note		= {ETH Dissertation No. 17097.},
  abstract	= {We present a semantic framework for object-oriented
		  specification languages. We develop this framework as a
		  conservative shallow embedding in Isabelle/HOL. Using only
		  conservative extensions guarantees by construction the
		  consistency of our formalization. Moreover, we show how our
		  framework can be used to build an interactive proof
		  environment, called HOL-OCL, for object-oriented
		  specifications in general and for UML/OCL in particular.
		  
		  Our main contributions are an extensible encoding of
		  object-oriented data structures in HOL, a datatype package
		  for object-oriented specifications, and the development of
		  several equational and tableaux calculi for object-oriented
		  specifications. Further, we show that our formal framework
		  can be the basis of a formal machine-checked semantics for
		  OCL that is compliant to the OCL 2.0 standard. },
  abstract_de	= {In dieser Arbeit wird ein semantisches Rahmenwerk f{\"u}r
		  objektorientierte Spezifikationen vorgestellt. Das
		  Rahmenwerk ist als konservative, flache Einbettung in
		  Isabelle/HOL realisiert. Durch die Beschr{\"a}nkung auf
		  konservative Erweiterungen kann die logische Konsistenz der
		  Einbettung garantiert werden. Das semantische Rahmenwerk
		  wird verwendet, um das interaktives Beweissystem HOL-OCL
		  f{\"u}r objektorientierte Spezifikationen im Allgemeinen
		  und insbesondere f{\"u}r UML/OCL zu entwickeln.
		  
		  Die Hauptbeitr{\"a}ge dieser Arbeit sind die Entwicklung
		  einer erweiterbaren Kodierung objektorientierter
		  Datenstrukturen in HOL, ein Datentyp-Paket f{\"u}r
		  objektorientierte Spezifikationen und die Entwicklung
		  verschiedener Kalk{\"u}le f{\"u}r objektorientierte
		  Spezifikationen. Zudem zeigen wir, wie das formale
		  Rahmenwerk verwendet werden kann, um eine formale,
		  maschinell gepr{\"u}fte Semantik f{\"u}r OCL anzugeben, die
		  konform zum Standard f{\"u}r OCL 2.0 ist.},
  pdf		= {http://www.brucker.ch/bibliography/download/2007/brucker-interactive-2007.pdf}
		  ,
  ps		= {http://www.brucker.ch/bibliography/download/2007/brucker-interactive-2007.ps.gz}
		  ,
  url		= {http://www.brucker.ch/bibliography/abstract/brucker-interactive-2007}
		  
}