by Achim D. Brucker
We briefly present the theorem proving environment HOL-OCL. The HOL-OCL system is an interactive proof environment for object-oriented (i.e., UML/OCL) specifications that is build on top of Isabelle/HOL. Overall, we introduce the overall system architecture and, in more detail, our extensible encoding of object-oriented data models into HOL.
While our extensible encoding is inspired by the extensible record package of Isabelle/HOL, its implementation is not directly based on it. In this talk, we will discuss how our approach differs from the existing one and discuss how it serves as a basis for implementing allows for implementing Isabelle-based tools for object-oriented models.
Keywords:
Categories:
Documents:
Please cite this article as follows:
Achim D. Brucker.
Encoding Object-oriented Datatypes in HOL: Extensible Records Revisited. Isabelle Developers Workshop (IDW), Cambridge, UK, 28. jun. 2010.
(slides) (handout) (BibTeX) (
abstract | = | {We briefly present the theorem proving environment HOL-OCL. The HOL-OCL system is an interactive proof environment for object-oriented (i.e., UML/OCL) specifications that is build on top of Isabelle/HOL. Overall, we introduce the overall system architecture and, in more detail, our extensible encoding of object-oriented data models into HOL.\\\\While our extensible encoding is inspired by the extensible record package of Isabelle/HOL, its implementation is not directly based on it. In this talk, we will discuss how our approach differs from the existing one and discuss how it serves as a basis for implementing allows for implementing Isabelle-based tools for object-oriented models.}, | |
address | = | {Cambridge, UK}, | |
author | = | {Achim D. Brucker}, | |
day | = | {28}, | |
event | = | {Isabelle Developers Workshop (IDW)}, | |
handout | = | {https://www.brucker.ch/bibliography/download/2010/talk-brucker-encoding-2010-2x2.pdf}, | |
isodate | = | {2010-06-18}, | |
lecturer | = | {Achim D. Brucker}, | |
month | = | {jun}, | |
slides | = | {https://www.brucker.ch/bibliography/download/2010/talk-brucker-encoding-2010.pdf}, | |
slideshare | = | {26244397}, | |
slideshare_height | = | {356}, | |
slideshare_width | = | {427}, | |
title | = | {Encoding Object-oriented Datatypes in HOL: Extensible Records Revisited}, | |
url | = | {https://www.brucker.ch/bibliography/abstract/talk-brucker-encoding-2010}, | |
year | = | {2010}, |