HOL-OCL 0.9.0 review

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

License: GPL (GNU General Public License) File size: 4671K Developer: Achim D. Brucker and Burkhart Wolff

0

HOL-OCL is an interactive proof environment for the Object Constraint Language (OCL). HOL-OCL project 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 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.