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)
svn checkout http://caml.inria.fr/svn/ocaml/branches/contracts
To build (bytecode) ocamlc:
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:
-scontract is for static contract checking only,
-dcontract is for dynamic contract checking only,
-hcontract is for hybrid contract checking.
|program||total LOC||Ann LOC||Time (sec)|
|arith, sum, max||26||4||0.30|
|AVL tree||328||12||491.75 (=8min11.75s)|