package gospel

  1. Overview
  2. Docs
A tool-agnostic formal specification language for OCaml

Install

Dune Dependency

Authors

Maintainers

Sources

gospel-0.1.0.tbz
sha256=4435d8a8f158edbc113bab01bbf4bb5e2a874bfa0a9b6b91bebcb95452c40464
sha512=4f1bc700bd0ee5aa4e035b18f253bc31880b0891cd27d55c2814ae7c7ad2c897fd804e1598201faa765b0ec1d61ee62c5d156c4ca2f6d40e77c82e95ac5c1f43

Description

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!

Published: 03 Nov 2021

README

README.md

Gospel

A tool-agnostic formal specification language for OCaml.

About

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!

We designed Gospel to provide a tool-agnostic frontend for bringing formal methods into the OCaml ecosystem, meaning that we make no assumptions on the future use of the specifications.

You can use Gospel specifications to complete and precise your documentation comments with non-ambiguous annotations and use a type-checker to ensure they always remain in sync. Other tools also rely on these annotations to provide additional features such as automated deductive verification or runtime assertion checking.

Please feel free to visit the project page if you wish to learn more about Gospel!

Getting Started

Installation

Gospel is not yet available on Opam repositories. You can install it via pinning:

$ opam pin add gospel.dev git@github.com:ocaml-gospel/gospel
$ opam install gospel

This will install the gospel tool binary, as well as the developer library if you wish to build your software on top of Gospel. You may check the installation with.

$ gospel --version
gospel version xxxxxx

Usage

Gospel contracts live in OCaml interface files (.mli), as special comments starting with the @ symbol:

val max_array: int array -> int
(*@ m = max_array a
    requires Array.length a > 0
    ensures forall i. 0 <= i < Array.length a -> a.(i) <= m
    ensures exists i. 0 <= i < Array.length a /\ a.(i) = m *)

Gospel provides a type-checker that ensures that your specifications are well-formed, well-typed, and remain in sync with the interface they annotate!

$ gospel check max_array.mli
OK

Tools using Gospel

At the moment, three tools leverage Gospel specifications to provide more guarantees to your programs:

  • Cameleer. A tool that extends Gospel to implementation files to provide semi-automated deductive verification of OCaml programs.

  • Ortac. A runtime assertion checking tool based that generates verifying code for your test suites or programs monitors.

  • Why3gospel. A Why3 plugin that lets you verify that a program proof refines the Gospel specifications before extracting it to OCaml.

License

This project is licensed under the MIT license.

See the LICENSE file for more information.

Authors

Gospel was initially developed by Cláudio Lourenço (LRI postdoctorate).

It is now maintained by Clément Pascutto, Mário Pereira, and Jean-Christophe Filliâtre.

The full list of contributors is available here.

Acknowledgements

This project is part of a collaboration between the LMF laboratory, Tarides, and NOVA LINCS.

The development is supported by:

  • The VOCaL project. ANR grant No. ANR-15-CE25-0008, 1/10/2015 - 31/3/2021.

  • The HORIZON 2020 Cameleer project (Marie Skłodowska-Curie grant agreement ID:897873) and NOVA LINCS (Ref. UIDB/04516/2020).

Dependencies (7)

  1. ppxlib >= "0.23.0" & < "0.26.0"
  2. ocaml-compiler-libs >= "v0.12.0"
  3. fmt >= "0.8.7"
  4. cmdliner >= "1.0.0"
  5. menhir >= "20181006"
  6. dune >= "2.4.0"
  7. ocaml >= "4.09"

Dev Dependencies

None

Used by

None

Conflicts

None