package gospel
Install
Dune Dependency
Authors
Maintainers
Sources
md5=e5b7f601526cbf590a070b6b9aebe1ad
sha512=a1375603a3f0ac7681e7e2e989be8af809edef78becc7d920e1d18af4f1db576dce91525cec70292c4ba559eb3f3bac67b023bcc826ea3dfdab956c86990ef91
Description
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!
Published: 12 Apr 2024
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!
type 'a t
(*@ model capacity : integer
mutable model contents : 'a sequence
with s
invariant s.capacity > 0
invariant Sequence.length s.contents <= s.capacity *)
exception Full
exception Empty
val create : int -> 'a t
(*@ s = create n
requires n > 0
ensures s.capacity = n
ensures s.contents = Sequence.empty *)
val is_empty : 'a t -> bool
(*@ b = is_empty s
pure
ensures b <-> s.contents = Sequence.empty *)
val clear : 'a t -> unit
(*@ clear s
modifies s.contents
ensures s.contents = Sequence.empty *)
val push : 'a -> 'a t -> unit
(*@ push a s
modifies s.contents
ensures s.contents = Sequence.cons a (old s.contents)
raises Full -> Sequence.length (old s.contents) = s.capacity
/\ s.contents = old s.contents *)
val pop : 'a t -> 'a
(*@ a = pop s
modifies s.contents
ensures a = Sequence.hd (old s.contents)
ensures s.contents = Sequence.tl (old s.contents)
raises Empty -> old s.contents = Sequence.empty = s.contents *)
val pop_opt : 'a t -> 'a option
(*@ o = pop_opt s
modifies s.contents
ensures match o with
| None -> old s.contents = Sequence.empty = s.contents
| Some a -> old s.contents = Sequence.cons a s.contents *)
val top : 'a t -> 'a
(*@ a = top s
ensures a = Sequence.hd s.contents
raises Empty -> s.contents = Sequence.empty *)
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 available on Opam repositories. Installing it is straightforward:
$ 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 0.2.0
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
Gospel also provides a ppx rewriter to allow odoc to display the contents of gospel specifications and declarations as documentation. This ppx rewriter works under the assumption that the source preprocessor has been run first. The dune stanza reads as follows:
(library
(name lib_name)
(preprocess
(pps gospel.ppx -- -pp "gospel pps")))
Be aware that it is the user's responsability to run the gospel type-checker when needed.
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 testing tool for OCaml programs that converts the Gospel specifications into code to test that they hold at runtime. You may use it to generate testing suites and fuzzers or monitor your program execution.
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 currently maintained by Jean-Christophe Filliâtre, Samuel Hym, Nicolas Osborne, Clément Pascutto, and Mário Pereira.
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 (11)
-
pp_loc
>= "2.1.0"
-
ppx_deriving
>= "5.2.1"
-
ppxlib
>= "0.26.0"
-
ocaml-compiler-libs
>= "v0.12.0"
-
fmt
>= "0.8.7"
-
cmdliner
>= "1.1.0"
-
menhir
>= "20181006"
- dune-build-info
-
dune
>= "3.0.0"
- ocamlfind
-
ocaml
>= "4.11"
Dev Dependencies (1)
-
odoc
with-test
Used by (2)
Conflicts
None