Static Contract Checking for Haskell

Papers

• Static Contract Checking for Haskell. In the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2009. (.pdf)
• Extended Static Checking for Haskell. In the ACM SIGPLAN Workshop on Haskell (Haskell), 2006. (.pdf)

Implementation

• Source code (based on the source code of ghc-6.9.2)

Hybrid Contract Checking for OCaml

Abstract

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.

Tutorial

Dynamic contract checking for OCaml (.pdf)

Papers

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)

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)