Static Contract Checking for Haskell



Hybrid Contract Checking for OCaml


Program errors are hard to detect or prove absent. Allowing programmers to write formal and precise specifications, especially in the form of contracts, is a popular approach to program verification and error discovery. We formalize and implement a hybrid (i.e. static and dynamic) contract checker for a pure subset of OCaml. The key technique is symbolic simplification, which makes integrating static and dynamic contract checking easy and effective. Our technique statically checks contract satisfaction or blames the function violating the contract. When a contract satisfaction is undecidable, it leaves residual code for dynamic contract checking.


Dynamic contract checking for OCaml (.pdf)


Hybrid Contract Checking via Symbolic Simplification. In the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM), 2012. (.pdf, INRIA technical report .pdf, journal version .pdf)


At the moment, you must have alt-ergo and ocamlgraph installed for static contract checking. We will embed alt-ergo source code which is written in OCaml in near future.


If you use the compiled ocamlc above, rename the downloaded bytecode to "ocamlc"

To compile an OCaml program to bytecode:

ocamlc -scontract -c
ocamlc -o program.byte program.cmo

To run the bytecode:


-scontract is for static contract checking only,
-dcontract is for dynamic contract checking only,
-hcontract is for hybrid contract checking.

Lastest implemetation and experiments (08Sept 2012)

Experiments are done on a PC running Ubuntu Linux with quadcore 2.93GHz CPU and 3.2 GB memory.
program total LOC Ann LOC Time (sec)
intro123, neg 23 4 0.13
mc91 4 1 0.14
ack, fhnhn 12 2 0.13
arith, sum, max 26 4 0.30
zipunzip 12 2 0.30
std/ 109 20 1.10
riser 33 3 0.13
insertion sort 52 2 0.09
selection sort 41 2 0.16
bubble sort 33 2 0.11
merge sort 57 7 1.29
quick sort 86 9 0.42
AVL tree 328 12 491.75 (=8min11.75s)
Redblack tree 154 10 4.18