IRILL - Research and Innovation on Free Software

Gospel and Ortac


"Gospel and Ortac"
by Clement Pascutto,
Download Webm format

Gospel is a behavioural specification language for OCaml program. It provides developers with a non-invasive and easy-to-use syntax to annotate their module interfaces with formal contracts that describe type invariants, mutability, function pre-conditions and post-conditions, effects, exceptions, and much more!