[ANN] Gospel 0.2.0

Ecosystem
1

We are very happy to announce the release 0.2.0 of gospel!

Gospel is a tool-agnostic behavioural specification language for OCaml. It allows you to write strongly typed contract-based specifications for your OCaml libraries (for a reasonable subset of OCaml). Gospel’s syntax has been designed to be easy to learn for an OCaml programmer. You can access the documentation here.

This release adds two main features, a gospel dumpast command and a gospel.ppx ppx rewriter to display Gospel specification as documentation with odoc.

Some minor extensions have been added to the language itself:

  • a with construct to name a variable in type invariants referring to a
    value of the specified type,
  • int literals,
  • anonymous functions now support both patterns in arguments and return type
    annotations,
  • unit result in function headers,
  • constants can now be referenced in specifications,
  • infix operators are now accepted in specification headers.

Parser, preprocessor, and error messages have been improved. In particular the preprocessor can now handle large files and locations are properly tracked. Pattern matches are now also checked for exhaustiveness and redundancy.

We have made a number of improvements and bugfixes in the type checker as well as some minor modifications in the Gospel standard library. Finally, the documentation has been revised.

15 Likes