Isabelle/HOL-OCL

HOL-OCL Logo

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 is developed by Achim D. Brucker and Burkhart Wolff.

HOL-OCL screenshot

HOL-OCL allows one to reason over OCL specifications, refine OCL specifications, and builds the basis for further tool support, e.g. for the automatic test-case generation.

HOL-OCL is free software; you can redistribute it and/or modify it under the terms of the GPL. It is developed by Achim D. Brucker and Burkhart Wolff

Download

hol-ocl-0.9.0.tar.gz (ca. 4.6 MiB, MD5: a41aa55362108d8141ec4d901844cc08) ChangeLog

Debian Packages

If you use the Debian GNU/Linux distribution, you can also install HOL-OCL using the following apt-repository:

deb http://kisogawa.inf.ethz.ch/isamorph/debian unstable main
deb-src http://kisogawa.inf.ethz.ch/isamorph/debian unstable main

Note: replace unstable by the distribution you are using, e.g., stable, testing, or unstable.

Related Publications

2014

2013

2012

2011

2010

2009

2008

2007

2006

2003

2002

2001