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

2020

• Achim D. Brucker, Frééric Tuong, and Burkhart Wolff. Model Transformation as Conservative Theory-Transformation. In J. Object Technol., 2020.
  Categories: ,
  (abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) ( )
  

2019

• 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) ( )
  

2017

• Robert Bill, Achim D. Brucker, Jordi Cabot Martin Gogolla, Antonio Vallecillo, and Edward D. Wilink. Workshop in OCL and Textual Textual Modelling: Report on Recent Trends and Panel Discussion. In STAF 2017 Workshops. Lecture Notes in Computer Science, 10748, pages 157-165, Springer-Verlag, 2017.
  Categories:
  (abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) ( )
  

2016

• 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) ( )
  

2015

• 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) ( )
  

2014

• Achim D. Brucker, Tony Clark, Carolina Dania, Geri Georg, Martin Gogolla, Frédéric Jouault, Ernest Teniente, and Burkhart Wolff. Panel Discussion: Proposals for Improving OCL. In Proceedings of the MODELS 2014 OCL Workshop (OCL 2014). CEUR Workshop Proceedings, 1285, pages 83-99, CEUR-WS.org, 2014.
  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. 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) ( )
  

2013

• 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) ( )
  

2012

• Achim D. Brucker and Burkhart Wolff. Featherweight OCL: A study for the consistent semantics of OCL 2.3 in HOL. In Workshop on OCL and Textual Modelling (OCL 2012). , pages 19-24, 2012. The semantics for the Boolean operators proposed in this paper was adopted by the OCL 2.4 standard.
  Categories: ,
  (abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1145/2428516.2428520) ( )
  

2011

• Matthias P. Krieger and Achim D. Brucker. Extending OCL Operation Contracts with Objective Functions. In Electronic Communications of the EASST, 44, 2011.
  Categories: ,
  (abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.14279/tuj.eceasst.44.662) (ECEASST) ( )
  

2010

• Achim D. Brucker, Matthias P. Krieger, Delphine Longuet, and Burkhart Wolff. A Specification-based Test Case Generation Method for UML/OCL. In MoDELS Workshops. Lecture Notes in Computer Science (6627), pages 334-348, Springer-Verlag , 2010. Selected best papers from all satellite events of the MoDELS 2010 conference. Workshop on OCL and Textual Modelling.
  Categories: ,
  (abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-642-21210-9_33) ( )
  

2009

• 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) ( )
  

2008

• 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) ( )
  

2007

• Achim D. Brucker. An Interactive Proof Environment for Object-oriented Specifications. ETH Zurich,2007. ETH Dissertation No. 17097.
  Categories: ,
  (abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) ( )
  

2006

• 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) ( )
  

2003

• Achim D. Brucker and Burkhart Wolff. Using Theory Morphisms for Implementing Formal Methods Tools. In Types for Proof and Programs. Lecture Notes in Computer Science (2646), pages 59-77, Springer-Verlag , 2003.
  Categories:
  (abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/3-540-39185-1_4) ( )
  

2002

• 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) ( )
  

2001

• Achim D. Brucker and Burkhart Wolff. Checking OCL Constraints in Distributed Systems Using J2EE/EJB. Albert-Ludwigs-Universität Freiburg, Technical Report 157, 2001.
  Categories:
  (abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) ( )
  
• Achim D. Brucker and Burkhart Wolff. Testing Distributed Component Based Systems Using UML/OCL. In Informatik 2001. Tagungsband der GI/ÖCG Jahrestagung, 1 (157), pages 608-614, 2001.
  Categories:
  (abstract) (full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) ( )