HOL-OCL 2.0

HOL-OCL 2.0 is a successor of HOL-OCL, an interactive proof environment for the Object Constraint Language (OCL). HOL-OCL 2.0 as a tool is based on a library defining its core semantic concepts called Featherweight OCL, which also serves as basis for the ongoing OCL 2.5 standardisation at the OMG.

HOL-OCL 2.0 addresses the fragment in UML concerned with object-oriented data modelling. Thus, it comes with a number of packages related with the semantic constructions and instantiations of objects, among other the Class Model Package to set up the underlying object-oriented datatype theory, or the Invariant & Operation Package supporting a formal contract language to define methods issued from a class model.

Authors

• Achim D. Brucker
• Frédéric Tuong
• Burkhart Wolff

License

This project is licensed under a 3-clause BSD-style license.

Publications

• Frédéric Tuong. Constructing Semantically Sound Object-Logics for UML/OCL Based Domain-Specific Languages. Université Paris-Sud, IRT SystemX, LRI, CNRS, CentraleSupélec, Université Paris-Saclay, 2016. https://tel.archives-ouvertes.fr/tel-01318156, Formal proof development.

• Frédéric Tuong, and Burkhart Wolff. A Meta-Model for the Isabelle API. In Archive of Formal Proofs, 2015. http://www.isa-afp.org/entries/Isabelle_Meta_Model.shtml, Formal proof development.

• 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.

• 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. https://www.brucker.ch/bibliography/abstract/brucker.ea-featherweight-2012