[ANN] Ortac 0.2.0, leverage Gospel formal specifications to generate tests

Ecosystem
1

We are very excited to announce this new Ortac release!

Ortac is a set of tools that translate Gospel specifications into OCaml code and use these translations to generate programs that check at runtime that the OCaml implementation respects the Gospel specifications.

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

This new release contains four packages:

  • ortac-core
  • ortac-runtime
  • ortac-qcheck-stm
  • ortac-runtime-qcheck-stm

The main improvements that brings this release concern the ortac-qcheck-stm plugin (the other three packages are mainly released for compatibility reasons).

ortac-qcheck-stm provides a plugin for Ortac. It generates QCheck-STM tests for a module specified with Gospel. QCheck-STM is a model-based testing framework and Ortac/QCheck-STM relies on the Gospel models you gave in the specifications to build the QCheck-STM tests.

I’d like to highlight two of these improvements.

The first one is that type invariants for what we call the system under test are now checked. Let’s say you want to generate QCheck-STM tests for a fixed-size container. You can give the following specification to your type:

type 'a t
(*@ mutable model contents : 'a list
    model size : int
    with t invariant List.length t.contents <= t.size *)

Now, the generated tests will check that the invariant is respected at initialisation of the system under test (the value of type 'a t) and that it is preserved by the functions being tested.

The second improvement concerns the test failure message. In order to make the failure more informative, a message stating which part of the Gospel specifications has been violated and a small OCaml program that demonstrates the unexpected behaviour will be displayed.

For example, with an artificial bug in the Array.length function, running the Ortac/QCheck-STM-generated test will print the following failure message:

random seed: 172339461
generated error fail pass / total     time test name
[✗]    1    0    1    0 / 1000     0.0s Array STM tests (generating)

--- Failure --------------------------------------------------------------------

Test Array STM tests failed (5 shrink steps):

   length sut


+++ Messages ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Messages for test Array STM tests:

Gospel specification violation in function length

  File "array.mli", line 7, characters 12-22:
    i = t.size
  
when executing the following sequence of operations:

  open Array
  let protect f = try Ok (f ()) with e -> Error e
  let sut = make 16 'a'
  let r = length sut
  assert (r = 16)
  (* returned 42 *)
  

================================================================================
failure (1 tests failed, 0 tests errored, ran 1 tests)

Although it has already helped find and fix some bugs, this project is still fairly new. So, feel free to try it and report any issue.

Happy testing!

9 Likes