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
Go to file
Frédéric Tuong 265943ddad update projects
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13653 3260e6d1-4efc-4170-b0a7-36055960796d
2019-03-08 09:01:41 +00:00
C11-FrontEnd implement dynamic storage of positions 2019-03-07 18:44:53 +00:00
doc update the generated files 2019-02-13 18:06:44 +00:00
examples remove global open 2019-02-25 17:19:20 +00:00
src store all encountered constructors in the environment 2019-01-10 18:37:56 +00:00
LICENSE update headers 2018-05-09 16:20:39 +00:00
LICENSE.thy update projects 2019-03-08 09:01:41 +00:00
LICENSE0.thy bootstrap 2018-05-22 17:13:59 +00:00
README.md document 2017-10-14 04:22:00 +00:00
README_advanced.txt upgrade to Isabelle2017 and afp-2017 2018-02-05 14:26:56 +00:00
ROOT update headers 2018-05-09 16:20:39 +00:00

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