An Interactive Proof Environment for Object-oriented Specifications

By Achim D. Brucker.

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.

Keywords:
OCL, UML, Formal Semantics, Theorem Proving, Isabelle, HOL-OCL

Supplementary material:
[ Slides  ]

Please cite this work as follows:
A. D. Brucker, “An interactive proof environment for object-oriented specifications,” PhD thesis, ETH Zurich, 2007. ETH Dissertation No. 17097.. Author copy: http://logicalhacking.com/publications/brucker-interactive-2007/

BibTeX
@PhDThesis{ brucker:interactive:2007,
  author      = {Achim D. Brucker},
  title       = {An Interactive Proof Environment for Object-oriented
                 Specifications},
  school      = {ETH Zurich},
  year        = {2007},
  month       = {mar},
  areas       = {formal methods, software},
  keywords    = {OCL, UML, Formal Semantics, Theorem Proving, Isabelle,
                 HOL-OCL},
  note        = {ETH Dissertation No. 17097.. 
                 Author copy: \url{http://logicalhacking.com/publications/brucker-interactive-2007/}},
  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.},
}