package ortac-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=26fe3888ccf1112c5961f50bbea8f427
sha512=27c75ad4a614c5e800d85714ef2e074dec9625ca78848dbc06823ad4a6d3e527d78600801bc94162bf24291c35eaa70ee83898e981ef2e5bbc703df249ffe077
Description
Ortac (OCaml Runtime Assertion Checking) is a tool to turn executable Gospel specifications into code to test they hold. Ortac Core provides:
- a library to turn Gospel terms and types into OCaml expressions and types,
- and a command-line tool. You will need at least one of the Ortac plugins to actually generate test code.
Published: 09 Jul 2024
README
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 theortac
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 theortac
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 theortac
command-line tool,ortac-monolith.opam
which provides the Monolith plugin for theortac
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.
Dependencies (8)
Dev Dependencies (3)
-
odoc
with-doc
-
ortac-runtime
with-test
-
alcotest
with-test & >= "0.8.1"
Used by (2)
Conflicts (1)
-
result
< "1.5"