[isabelle] Proving OCL constraints with Isabelle



This post is not to seek for help, it's to share something which may be of interest to people.

That's additional elements to be used with Isabelle, to be able to formally prove constraints expressed in the OCL language, the one used for formal specifications in UML diagram (or textual HUTN source) and MOF.

http://www.brucker.ch/projects/hol-ocl/

Seems old, as the page proudly shows the obsolete old Isabelle UI, the one based on Emacs. The package was indeed last updated 2006-08-15, so there may be issues. I have not tested it.


--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.