HOL-OCL is an interactive proof environment for the Object Constraint Language (OCL).
Version: 0.9.0HOL-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.
Operating System: Linux
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.