Hybrid Contract Checking for OCaml

Abstract

Program errors are hard to detect and to prove absent. Contract checking allows us to (a) statically verify that a function satisfies its contract; (b) precisely blame functions at fault both statically and dynamically when there is a contract violation. Static contract checking catches all bugs but can only check restricted properties while dynamic checking can check more expressive properties, but is not complete. In this project, we integrate static and dynamic contract checking for a subset of OCaml. We exploit a static checker as much as possible and leave the residual contract satisfaction checks to run-time. Thus, no (potential) bugs can escape and yet expressive properties can be expressed.

Tutorial

Dynamic contract checking for OCaml (.pdf)

Papers

Hybrid contract checking via symbolic simplification (.pdf, INRIA technical report .pdf, HOSC .pdf)

Download

• Source code (based on the source code of ocamlc-3.12.1):
  

  svn checkout http://caml.inria.fr/svn/ocaml/branches/contracts

  To build (bytecode) ocamlc:
  
  cd contracts
  ./configure
  make coldstart
  make ocamlc
  

• Linux
  

  bytecode: ocamlc-linux

• Mac
  

  bytecode: ocamlc-mac

Instructions

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

To compile an OCaml program to bytecode:

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

To run the bytecode:

./program.byte

Options
-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)