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

Related Publications

2020

2019

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2003

2002

2001