`ortac` — OCaml RunTime Assertion Checking

ortac is a tool to convert an OCaml module interface with Gospel
specifications into code to check those specifications.

There are various ways to check specifications, all provided by plugins.

The QCheck-STM plugin generates a program using QCheck-STM that will test
the module by running random functions calls and checking they give consistent
results with the model provided in the Gospel specification; see the dedicated
README for details.

This repository also contains two other experimental plugins, that are not yet
stable. Expect rough edges if you venture to try them out:

the wrapper plugin generates wrapper modules, i.e. modules
exposing the original interface but instrumenting all function calls
with assertions on arguments and on results, either normal or
exceptional; see the dedicated README for
details,
the monolith plugin generates programs using Monolith that will
test a module by comparing it against an instrumented version of
that module; see the dedicated README for
details.

At its core, Ortac provides a way to convert the executable fragment of Gospel
into OCaml code. This core functionality is used by all plugins.

Installation

The easiest way to try ortac out is to opam install its main packages
directly from the opam repository:

opam install ortac-qcheck-stm ortac-runtime

This will install the following OPAM packages:

ortac-core.opam which provides the ortac command-line tool and the core
functionality used by all plugins,
ortac-runtime.opam which provides the support library for the code
generated by Ortac plugins,
ortac-qcheck-stm.opam which provides the QCheck-STM plugin for the
ortac command-line tool.

Alternatively, you can install the packages directly from this repository using
opam pin:

opam pin add -y https://github.com/ocaml-gospel/ortac.git

Besides the first three packages, this will also install the following
experimental packages:

ortac-wrapper.opam which provides the wrapper plugin for the ortac
command-line tool,
ortac-monolith.opam which provides the Monolith plugin for the
ortac command-line tool,
ortac-runtime-monolith.opam which provides the support library for
the code generated with the Monolith plugin.
ortac-dune.opam which provides a dune rule generator.

Even using opam pin, you can install only some of those packages by explicitly
mentioning which package you want to install, for instance:

$ opam pin add ortac-core https://github.com/ocaml-gospel/ortac.git

To check that it is correctly installed, simply run ortac. If you
installed all packages, you should get:

$ ortac
ortac: required COMMAND name is missing, must be one of 'monolith', 'qcheck-stm' or 'wrapper'.
Usage: ortac COMMAND …
Try 'ortac --help' for more information.

Quick start

or: How to use Ortac to test whether the specifications of a module
hold.

QCheck-STM plugin

The QCheck-STM plugin can generate a standalone executable that will
test the consistency between the behaviour of the functions of the
module and their model, as provided by the Gospel specifications. Look
at the dedicated README for the QCheck-STM plugin
to see how it can be used.

Monolith plugin

The Monolith plugin can generate a standalone executable that will try
to falsify the Gospel specifications of a module by stress-testing the
code. Look in the dedicated README for the Monolith
plugin to see how it can be used.

Wrapper plugin

The wrapper plugin can be used to generate a wrapper module that
will expose the same interface as the original module but
instrumenting all function calls with assertions corresponding to the
Gospel specifications. Look in the dedicated README
for the wrapper plugin to see how it can be used.

Supported Gospel

The main general limitation on what Gospel specifications are supported comes
from the translation from Gospel into OCaml: it is only possible to translate
the executable fragment of the Gospel language. In particular, it does not
support quantifications except in the very specific patterns in which they
quantify over an integer within explicit bounds such as:

forall i. a < i < b -> ...
exists i. a < i < b /\ ...

(the pattern matching tolerates some small variations in the way bounds are
stated, such as b >= i > a, etc. but not much more).

Additionally, each plugin has its own set of constraints on what it
can handle. See the dedicated READMEs for details.

Found issues

The QCheck-STM plugin has already proven itself useful as it has discovered a
number of issues:

ortac — OCaml RunTime Assertion Checking