Alright. After much waiting and detours, I’ve finally decided to start doing some original work in Isabelle/HOL itself. *drum rolls*

After the last meeting with Mr. MM, I’ve decided to start working on the specification I’ve already done in Z of his framework. The specification is pretty involved and would require much more work to be properly embedded in HOL. I have a few ideas but that will have to wait.

Mr. MM: Here’s my plan. First of all, what needs to be done is that we need to have the Document Model formalized, specified and verified. This has already been done during HOL-OCL development by the ETH Zurich guys but I would like to do it in a more accessible way (i.e. without the use of stuff like “smashed sets and objects”). I want to make something that can be used by the average formal specification engineer. If we can get only this done, it would be an accomplishment.

So, I would appreciate it if you can take some time out and find out for me if the Class Diagrams of UML have been formalized in Isabelle/HOL. I’ve done thorough searching and have only found stuff done in either HOL-Z or HOL-OCL (all by the ETH guys). I want to make sure that I’m not re-inventing the wheel. I’ll continue my search but it would be a big help if you can confirm that it has not been done before or find me the papers which have done it.