Formal Methods

Installing and Configuring HOL-OCL

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:


Install SML/NJ
Take a look at INSTALL  — it’s helpful but verbose and not accurate about basic installation

Get these files:
    boot.<arch>.<os>.tgz  (boot.x86.unix.tgz)

  1. Create a folder temp for installation source
  2. Unpack config.tgz to config
  3. Put config in temp
  4. 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!
  5. Copy other two tgz files to temp/ folder
  6. Go to temp folder
  7. Rename the main folder containing everything to smlnj
  8. Copy this folder to Isabelle_home/contrib/
  9. Run

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
Java jar file. Easy to run. Works beautifully

Get Dresden OCL1.2 for OCL2
run using: java -jar ocl20parsertools.jar

Take a look at their Publications
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.


2 thoughts on “Installing and Configuring HOL-OCL”

Comments are closed.