Experimental mirror of Citadelle ( https://projects.brucker.ch/hol-testgen/log/trunk/hol-testgen/add-ons/Featherweight-OCL ) compiling with randomly selected versions of Isabelle
Frédéric Tuong 6739ac8159 Merge branch 2017 into devel 1 month ago
doc update the generated files 4 months ago
examples Merge branch 2017 into devel 2 months ago
src Merge branch 2017 into devel 1 month ago
LICENSE update headers 6 months ago
LICENSE.thy simplify 4 months ago
LICENSE0.thy continue 670771027c 4 months ago
README.md document 1 year ago
README_advanced.txt upgrade to Isabelle2017 and afp-2017 9 months ago
ROOT upgrade to Isabelle devel/28f9e9b80c and afp-devel 4 months ago
ROOTS upgrade to Isabelle devel/28f9e9b80c and afp-devel 4 months ago

README.md

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

License

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

Publications