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.
Open source project that offer summary and download services on this page is a project that carry out their development work on other open source development sites. Their work is linked to this page via a feature called OFI, and their work is not carried out here on OSDN site.
