gospelversion Documentation on ocaml.org
A tool-agnostic formal specification language for OCaml
Gospel is a behavioural specification language for OCaml programs. 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!
| Authors | Jean-Christophe Filliâtre, Samuel Hym, Cláudio Lourenço, Nicolas Obsorne, Clément Pascutto and Mário Pereira |
|---|---|
| License | MIT |
| Published | |
| Homepage | https://github.com/ocaml-gospel/gospel |
| Issue Tracker | https://github.com/ocaml-gospel/gospel/issues |
| Maintainer | Jean-Christophe.Filliatre@lri.fr |
| Dependencies |
|
| Source [http] | https://github.com/ocaml-gospel/gospel/archive/refs/tags/v0.3.1.tar.gz md5=99432da6253cc1d5eb071caa635044a1 sha512=a50035d28c10119b0d42391fcf1cce4cab101170f6ed308bfd214165b09e595d817fc0eea0efb4632810bd962cad022473ff9148bccd4854e46c22462347702e |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/gospel/gospel.0.3.1/opam |
No package is dependent
