[ANN] Ortac 0.5.0 testing higher order functions

Ecosystem
,
1

Hi everyone!

I’m very pleased to announce the release of the Ortac-0.5.0 packages for specification-driven testing!

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

This new release brings three new features.

In the effort to increase the coverage of the generated tests and thanks to Jan Midtgaard, we now support testing higher order functions. Thanks Jan!

It is also now possible to test a module exposed as a sub-module by Dune, specifying the module’s prefix in a CLI optional argument. A feature that we’ve been asked to add.

And to test an actual sub-module defined inside an OCaml file, specifying the sub-module in a CLI optional argument as well.

Ortac/Dune generates the Dune boilerplate for you. It has been updated to support the two new optional arguments.

You can install those packages via opam:

$ opam install ortac-qcheck-stm ortac-dune

Then you write some Gospel specifications in your library’s interface file foo.mli:

type 'a t
(*@ mutable model contents : 'a sequence *)

val make : int -> 'a -> 'a t
(*@ t = make i a
    ensures t.contents = Sequence.init i (fun _ -> a) *)

val for_all : ('a -> bool) -> 'a t -> bool
(*@ b = for_all p t
    ensures b = Sequence.fold_left (fun acc a -> acc && p a) true t.contents *)

Then a simple configuration file foo_config.ml:

type sut = char t

let init_sut = make 42 'a'

And you can generate some specification-driven model-based tests for your library just by running:

$ ortac qcheck-stm foo.mli foo_config.ml

If you want to integrate the generation and the running of the tests to your dune setup (which is highly recommended), just add the following stanza to your dune file in your test directory:

(rule
 (alias runtest)
 (mode promote)
 (action
  (with-stdout-to
   dune.inc
   (run ortac dune qcheck-stm foo.mli))))

(include dune.inc)

You’ll find more information in the Ortac/QCheck-STM documentation, the Ortac/Dune README and the examples folder. I’m also happy to answer questions.

Happy testing!

10 Likes