You cannot select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
Frédéric Tuong 6212dc4dcd split C_File.command
git-svn-id: 3260e6d1-4efc-4170-b0a7-36055960796d
4 years ago
C11-FrontEnd split C_File.command 4 years ago
doc update the generated files 4 years ago
examples remove global open 4 years ago
src store all encountered constructors in the environment 4 years ago
LICENSE update headers 5 years ago
LICENSE.thy update projects 4 years ago
LICENSE0.thy bootstrap 5 years ago document 6 years ago
README_advanced.txt upgrade to Isabelle2017 and afp-2017 5 years ago
ROOT update headers 5 years ago


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.



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