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 screenshot

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 MByte, MD5: a41aa55362108d8141ec4d901844cc08) ChangeLog

Debian Packages

If you use the Debian GNU/Linux distribution, you can also install HOL-OCL using the following apt-repository:

deb http://kisogawa.inf.ethz.ch/isamorph/debian unstable main
deb-src http://kisogawa.inf.ethz.ch/isamorph/debian unstable main

Note: replace unstable by the distribution you are using, e.g., stable, testing, or unstable.

Related Publications

2009

Achim D. Brucker and Matthias P. Krieger and Burkhart Wolff. Extending OCL with Null-References. In Models in Software Engineering (MoDELS 2009 Workshops). Lecture Notes in Computer Science, Springer-Verlag , 2009. Selected best papers from all satelite events of the MoDELS 2009 conference.
Categories: ,
(abstract) (PDF) (BibTeX) (Endnote) (RIS) ( )
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) (PDF) (BibTeX) (Endnote) (RIS) (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) (PDF) (BibTeX) (Endnote) (RIS) (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) (PDF) (BibTeX) (Endnote) (RIS) (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) (PDF) (BibTeX) (Endnote) (RIS) (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) (PDF) (BibTeX) (Endnote) (RIS) ( )

2006

Achim D. Brucker and 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) (PDF) (Extended Version) (BibTeX) (Endnote) (RIS) (doi:10.1007/11880240_22) ( )
Achim D. Brucker and Jürgen Doser and Burkhart Wolff. A Model Transformation Semantics and Analysis Methodology for SecureUML. ETH Zurich, Technical Report 524, 2006.
Categories: , ,
(abstract) (PDF) (BibTeX) (Endnote) (RIS) ( )
Achim D. Brucker and Jürgen Doser and Burkhart Wolff. An MDA Framework Supporting OCL. In Electronic Communications of the EASST, 5, 2006.
Categories: , ,
(abstract) (PDF) (BibTeX) (Endnote) (RIS) (ECEASST) ( )
Achim D. Brucker and Jürgen Doser and Burkhart Wolff. Semantic Issues of OCL: Past, Present, and Future. In Electronic Communications of the EASST, 5, 2006.
Categories: ,
(abstract) (PDF) (BibTeX) (Endnote) (RIS) (ECEASST) ( )
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). Computing Research Repository (CoRR), 2006.
Categories: ,
(abstract) (PDF) (BibTeX) (Endnote) (RIS) ( )
Achim D. Brucker and Burkhart Wolff. The HOL-OCL Book. ETH Zurich, Technical Report 525, 2006.
Categories: ,
(abstract) (PDF) (BibTeX) (Endnote) (RIS) ( )

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) (PDF) (BibTeX) (Endnote) (RIS) (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) (PDF) (BibTeX) (Endnote) (RIS) (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 2003). Lecture Notes in Computer Science (2410), pages 99-114, Springer-Verlag , 2002.
Categories: ,
(abstract) (PDF) (extended) (BibTeX) (Endnote) (RIS) (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) (PDF) (BibTeX) (Endnote) (RIS) ( )

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) (PDF) (BibTeX) (Endnote) (RIS) ( )
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) (PDF) (BibTeX) (Endnote) (RIS) ( )