[ANN] Ortac/QCheck-STM 0.4.0 Dynamic formal verification beyond one system under test

Hi everyone!

I’m very pleased to announce this exciting new release of ortac-qcheck-stm.0.4.0!

This new release brings some exciting new features, mostly the result of Nikolaus Huber’s contributions! Thank you Nik!

Ortac/QCheck-STM is a test generator based on the QCheck-STM model-based testing framework and the Gospel specification language for OCaml.

You can find the project on this repo and install the released packages via opam.

It is also encourage to install ortac-dune to avoid having to write too much dune boilerplate.

In particular, this release extend Ortac/QCheck-STM so that the generated tests will include functions that can take multiple System-Under-Tests as argument and/or that can return one. So now, if we write Gospel specifications for append-like functions, Ortac/QCheck-STM will include them in the generated tests!

Happy testing!

7 Likes