[isabelle] ANN: First Public Release of HOL-OCL

We are happy to announce the first public version of

                  HOL-OCL, version 0.9.0

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.

HOL-OCL is distributed under the GNU General Public License (GPL) and
can be downloaded from the HOL-OCL web site at:


Kind regards,
    Achim D. Brucker and Burkhart Wolff
Achim D. Brucker, Information Security, IFW C 41.2, ETH Zentrum, 8092 Zurich
 Phone: +41 44 63 25217, Fax: +41/44 63 21172, http://www.brucker.ch
          brucker at inf.ethz.ch (preferable GPG/PGP encrypted)

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.