Hi everyone!
I’m very pleased to announce this exciting new release of Ortac packages!
Ortac is a set of tools for dynamic verification of Gospel formal specifications of OCaml code.
You can find the project on this repo and install the released packages via opam.
Released packages are:
ortac-coreortac-runtimeortac-runtime-qcheck-stmortac-qcheck-stmortac-dune
But running:
$ opam install ortac-qcheck-stm ortac-dune
should be enough to install what is necessary.
Apart from some fixes, this release brings three main improvements to the Ortac/QCheck-STM mode.
The first one is about user experience. This is a two-parts improvement as we:
- move to a module-based configuration to reduce the number of arguments to give
ortac qcheck-stmwhile increasing the flexibility of configuration (see documentation for more information) - release the Ortac/Dune plugin which generates the dune rules necessary to generate and run the tests (see README for usage).
With these two improvements, we believe that you have a very good excuse for not writing tests: it is very easy to generate them!
The second improvement is related to the supported subset of Gospel, mainly about how you can express the logical model for your OCaml types: you don’t have to limit yourself anymore to the Gospel standard library.
Finally, some work has been put on extending the coverage of the generated tests: functions without any SUT argument and functions mentioning tuples are now included in the tested values.
Happy testing!