Mac Categories

HOL-OCL 0.9.0


HOL-OCL HOL-OCL - Interactive proof environment for the Object Constraint Language (OCL)

System Requirememts
Mac OS X
Download Details
Company Achim D. Brucker and Burkhart Wolff
Version 0.9.0
Post Date September 18, 2009
License GPL
File Size 4.6 MB
There are no screenshots

HOL-OCL 0.9.0


HOL-OCL - Interactive proof environment for the Object Constraint Language (OCL)
HOL-OCL is an interactive proof environment for the Object Constraint Language (OCL).

HOL-OCL is implemented as a shallow embedding of OCL into the Higher-order Logic (HOL) instance of the interactive theorem prover Isabelle.

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