Isabelle/HOL-OCL
HOL-OCL is an interactive proof environment for the Object Constraint Language (OCL). It is implemented as a shallow embedding of OCL into the Higher-order Logic (HOL) instance of the interactive theorem prover Isabelle. HOL-OCL is developed by Achim D. Brucker and Burkhart Wolff.
HOL-OCL allows one to reason over OCL specifications, refine OCL specifications, and builds the basis for further tool support, e.g. for the automatic test-case generation.
HOL-OCL is free software; you can redistribute it and/or modify it under the terms of the GPL. It is developed by Achim D. Brucker and Burkhart Wolff
Download
hol-ocl-0.9.0.tar.gz
(ca. 4.6 MiB, MD5: a41aa55362108d8141ec4d901844cc08)
ChangeLog
Related Publications
-
Achim D. Brucker, Gwendal Daniel, Martin Gogolla, Frédéric Jouault, Christophe Ponsard,, Valéry Ramon, and Edward D. Willink.
Emerging Topics in Textual Modelling.
In OCL 2019. CEUR Workshop Proceedings, 2513, pages 91-104, CEUR-WS.org, 2019.
Categories:
(abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Achim D. Brucker, Jordi Cabot, Gwendal Daniel, Martin Gogolla, Adolfo Sánchez-Barbudo Herrera, Frank Hilken, Frédéric Tuong, Edward D. Willink, and Burkhart Wolff.
Recent Developments in OCL and Textual Modelling.
In Proceedings of the International Workshop on OCL and Textual Modeling (OCL 2016). CEUR Workshop Proceedings, 1756, pages 157-165, CEUR-WS.org, 2016.
Categories:
(abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Achim D. Brucker, Frédéric Tuong, and Burkhart Wolff.
Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5. LRI, Univ Paris Sud, CNRS, Centrale Supélec, Université Paris-Saclay, France, Technical Report 1582, 2015.
Categories: ,
(abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Frédéric Tuong and Burkhart Wolff.
A Meta-Model for the Isabelle API.
In Archive of Formal Proofs, 2015.
(BibTeX) (Endnote) (RIS) (Word) (URL) ( )
-
Achim D. Brucker, Frédéric Tuong, and Burkhart Wolff.
Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5.
In Archive of Formal Proofs, 2014. http://www.isa-afp.org/entries/Featherweight_OCL.shtml, Formal proof development
Categories: ,
(abstract) (full text as PDF file) (Outline) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Delphine Longuet, Frédéric Tuong, and Burkhart Wolff.
Towards a Tool for Featherweight OCL: A Case Study On Semantic Reflection.
In Proceedings of the MODELS 2014 OCL Workshop (OCL 2014). CEUR Workshop Proceedings, 1285, pages 43-52, CEUR-WS.org, 2014.
(abstract) (BibTeX) (Endnote) (RIS) (Word) (URL) ( )
-
Achim D. Brucker, Dan Chiorean, Tony Clark, Birgit Demuth, Martin Gogolla, Dimitri Plotnikov, Bernhard Rumpe, Edward D. Willink, and Burkhart Wolff.
Report on the Aachen OCL Meeting.
In Proceedings of the MODELS 2013 OCL Workshop (OCL 2013). CEUR Workshop Proceedings, 1092, pages 103-111, CEUR-WS.org, 2013.
Categories:
(abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Achim D. Brucker, Delphine Longuet, Frédéric Tuong, and Burkhart Wolff.
On the Semantics of Object-oriented Data Structures and Path Expressions.
In Proceedings of the MODELS 2013 OCL Workshop (OCL 2013). CEUR Workshop Proceedings, 1092, pages 23-32, CEUR-WS.org, 2013. An extended version of this paper is available as LRI Technical Report 1565.
Categories: ,
(abstract) (full text as PDF file) (Extended Version) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Achim D. Brucker, Delphine Longuet, Frédéric Tuong, and Burkhart Wolff.
On the Semantics of Object-oriented Data Structures and Path Expressions (Extended Version). Laboratoire en Recherche en Informatique (LRI), Université Paris-Sud 11, France, Technical Report 1565, 2013.
Categories: ,
(abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Achim D. Brucker, Matthias P. Krieger, and Burkhart Wolff.
Extending OCL with Null-References.
In Models in Software Engineering. Lecture Notes in Computer Science (6002), pages 261-275, Springer-Verlag , 2009. Selected best papers from all satellite events of the MoDELS 2009 conference.
Categories: ,
(abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-642-12261-3_25) ( )
-
Achim D. Brucker and Burkhart Wolff.
Semantics, Calculi, and Analysis for Object-oriented Specifications.
In Acta Informatica, 46 (4), pages 255-284, 2009.
Categories: ,
(abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/s00236-009-0093-8) ( )
-
Achim D. Brucker and Burkhart Wolff.
HOL-OCL - A Formal Proof Environment for UML/OCL.
In Fundamental Approaches to Software Engineering (FASE08). Lecture Notes in Computer Science (4961), pages 97-100, Springer-Verlag , 2008.
Categories: ,
(abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-540-78743-3_8) ( )
-
Achim D. Brucker and Burkhart Wolff.
Extensible Universes for Object-oriented Data Models.
In ECOOP 2008 - Object-Oriented Programming. Lecture Notes in Computer Science (5142), pages 438-462, Springer-Verlag , 2008.
Categories: ,
(abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-540-70592-5_19) ( )
-
Achim D. Brucker and Burkhart Wolff.
An Extensible Encoding of Object-oriented Data Models in HOL.
In Journal of Automated Reasoning, 41, pages 219-249, 2008.
Categories: ,
(abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/s10817-008-9108-3) ( )
-
Achim D. Brucker, Jürgen Doser, and Burkhart Wolff.
A Model Transformation Semantics and Analysis Methodology for SecureUML.
In MoDELS 2006: Model Driven Engineering Languages and Systems. Lecture Notes in Computer Science (4199), pages 306-320, Springer-Verlag , 2006. An extended version of this paper is available as ETH Technical Report, no. 524.
Categories: , ,
(abstract) (full text as PDF file) (Extended Version) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/11880240_22) ( )
-
Achim D. Brucker, Jürgen Doser, and Burkhart Wolff.
A Model Transformation Semantics and Analysis Methodology for SecureUML. ETH Zurich, Technical Report 524, 2006.
Categories: , ,
(abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Achim D. Brucker, Jürgen Doser, and Burkhart Wolff.
An MDA Framework Supporting OCL.
In Electronic Communications of the EASST, 5, 2006.
Categories: , ,
(abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.14279/tuj.eceasst.5.45) ( )
-
Achim D. Brucker, Jürgen Doser, and Burkhart Wolff.
Semantic Issues of OCL: Past, Present, and Future.
In Electronic Communications of the EASST, 5, 2006.
Categories: ,
(abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:http://dx.doi.org/10.14279/tuj.eceasst.5.46) ( )
-
Achim D. Brucker and Burkhart Wolff.
A Package for Extensible Object-Oriented Data Models with an Application to IMP++.
In International Workshop on Software Verification and Validation (SVV 2006), 2006.
Categories: ,
(abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Achim D. Brucker and Burkhart Wolff.
The HOL-OCL Book. ETH Zurich, Technical Report 525, 2006.
Categories: ,
(abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Achim D. Brucker and Burkhart Wolff.
HOL-OCL: Experiences, Consequences and Design Choices.
In UML 2002: Model Engineering, Concepts and Tools. Lecture Notes in Computer Science (2460), pages 196-211, Springer-Verlag , 2002.
Categories: ,
(abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/3-540-45800-X_17) ( )
-
Achim D. Brucker and Burkhart Wolff.
A Proposal for a Formal OCL Semantics in Isabelle/HOL.
In Theorem Proving in Higher Order Logics (TPHOLs). Lecture Notes in Computer Science (2410), pages 99-114, Springer-Verlag , 2002.
Categories: ,
(abstract) (full text as PDF file) (Extended Version) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/3-540-45685-6_8) ( )
-
Achim D. Brucker and Burkhart Wolff.
A Note on Design Decisions of a Formalization of the OCL. Albert-Ludwigs-Universität Freiburg, Technical Report 168, 2002.
Categories: ,
(abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) ( )