I’ve just finished installing/configuring HOL-OCL (except for the X-symbols configuration). This was a pretty complex process and the documentation is pretty scattered. Here’s the flow I followed:
Get HOL-OCL
- Download HOL-OCL from:http://www.brucker.ch/projects/hol-ocl/
- Need SML/NJ because of some datatype deficiency in Poly/ML
Install SML/NJ
From: http://www.smlnj.org/dist/working/110.56/index.html
Take a look at INSTALL – it’s helpful but verbose and not accurate about basic installation
Get these files:
config.tgz
boot.<arch>.<os>.tgz (boot.x86.unix.tgz)
runtime.tgz
smlnj-lib.tgz
MLRISC.tgz
ml-yacc.tgz
ml-lex.tgz
cml.tgz
- Create a folder temp for installation source
- Unpack config.tgz to config
- Put config in temp
- Put from temp/config/* to temp/* – I don’t think all files are needed here. I just haven’t got around to finding which ones are!
- Copy other two tgz files to temp/ folder
- Go to temp folder
- Rename the main folder containing everything to smlnj
- Copy this folder to Isabelle_home/contrib/
- Run install.sh
Setting up Isabelle to Use HOL+OCL
Take a look at Section 7.2.1 of HOL-OCL Book
After copying smlnj folder to isabelle_home/contrib/:
Recompile Isabelle using sml/nj :
Overwrite $hol-ocl_dir$/contrib/defs.ML to $isabelle_home$/src/Pure/defs.ML – you can get this file from the hol-ocl installation folder
edit: /usr/local/Isabelle2005/etc/settings – uncomment smlnj portion, comment out polyml portion
Go to isabelle_home
build -m HOL-Complex HOL
this may take a while … sml/nj is a little slow during compilation
get Hol-ocl
Extract to isabelle_home/
Go to isabelle_home/hol-ocl-0.9.0/src
isatool make
set environment variable HOLOCL_HOME
Get ArgoUML
http://argouml.tigris.org/
Java jar file. Easy to run. Works beautifully
Get Dresden OCL1.2 for OCL2
From: http://dresden-ocl.sourceforge.net/index.html
run using: java -jar ocl20parsertools.jar
Take a look at their Publications
http://www.brucker.ch/projects/hol-ocl/
A Model Transformation Semantics and Analysis Methodology for SecureUML.
And now that I’ve done it, I’m not sure I’m going to use it but I may give it a try. It seems promising for a specific area of application of formal methods.