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.

Further Reading:
This presentation is based on the following publication:
A. D. Brucker, “An interactive proof environment for object-oriented specifications,” PhD thesis, ETH Zurich, 2007. ETH Dissertation No. 17097.. Author copy: https://logicalhacking.com/publications/brucker-interactive-2007/

Please cite this work as follows:
A. D. Brucker, “An interactive proof environment for object-oriented specifications,” presented at the Ph.d. defense, ETH Zurich, Zurich, Switzerland, Mar. 09, 2007. Author copy: https://logicalhacking.com/publications/talk-brucker-interactive-2007/

BibTeX
@Unpublished{ talk:brucker:interactive:2007,
  date       = {2007-03-09},
  author     = {Achim D. Brucker},
  title      = {An Interactive Proof Environment for Object-oriented
                Specifications},
  lecturer   = {Achim D. Brucker},
  venue      = {ETH Zurich, Zurich, Switzerland},
  eventtitle = {Ph.D. Defense},
  language   = {USenglish},
  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.},
  areas      = {software, formal methods},
  note       = {Author copy: \url{https://logicalhacking.com/publications/talk-brucker-interactive-2007/}},
  pdf        = {https://logicalhacking.com/publications/talk-brucker-interactive-2007/talk-brucker-interactive-2007.pdf},
}