Email Gateway (Aug 18 2022 at 09:33): Email Gateway (Aug 18 2022 at 09:33):From: "Achim D. Brucker" <brucker@spamfence.net>
We are happy to announce the first public version of
HOL-OCL, version 0.9.0
http://www.brucker.ch/projects/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 defines a machine-checked formalization of the semantics as
described in the standard for OCL 2.0. This conservative, shallow
embedding of UML/OCL into Isabelle/HOL includes support for typed,
extensible UML data models supporting inheritance and subtyping inside
the typed lambda-calculus with parametric polymorphism. As a
consequence of conservativity with respect to higher-order logic
(HOL), we can guarantee the consistency of the semantic model.
Moreover, HOL-OCL provides several derived calculi for UML/OCL that
allow for formal derivations establishing the validity of UML/OCL
formulae. Elementary automated support for such proofs is also provided.
Several papers describing HOL-OCL in detail are also available from
the HOL-OCL website. In particular we recommend "The HOL-OCL Book"
as a general textbook on formal OCL semantics as well as a
a main reference and system manual:
A. D. Brucker and B. Wolff. The HOL-OCL Book. Tech. Rep. 525, ETH
Zurich, 2006.
http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-book-2006
HOL-OCL is distributed under the GNU General Public License (GPL) and
can be downloaded from the HOL-OCL web site at:
http://www.brucker.ch/research/hol-ocl/
Kind regards,
Achim D. Brucker and Burkhart Wolff
Last updated: May 03 2024 at 12:27 UTC