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!

AuthorsJean-Christophe Filliâtre, Samuel Hym, Cláudio Lourenço, Nicolas Obsorne, Clément Pascutto and Mário Pereira
LicenseMIT
Published
Homepagehttps://github.com/ocaml-gospel/gospel
Issue Trackerhttps://github.com/ocaml-gospel/gospel/issues
MaintainerJean-Christophe.Filliatre@lri.fr
Dependencies
Source [http] https://github.com/ocaml-gospel/gospel/archive/refs/tags/0.2.0.tar.gz
md5=964e7cb82b4391c7ad0794c20adcc67f
sha512=15c5d3f48fac648ce0799c2664323d461f3792ae9477ba0fe8c499228a9faddda22e8ef66ef10733dce550dcf8ba2641fce2b5472005f649f28e5426d0631375
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/gospel/gospel.0.2.0/opam