gospelversion
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/0.3.0.tar.gz md5=e5b7f601526cbf590a070b6b9aebe1ad sha512=a1375603a3f0ac7681e7e2e989be8af809edef78becc7d920e1d18af4f1db576dce91525cec70292c4ba559eb3f3bac67b023bcc826ea3dfdab956c86990ef91 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/gospel/gospel.0.3.0/opam |
Required by
- ortac-core>=0.2.0
- ortac-qcheck-stm>=0.2.0
