Ortac/QCheck-STM

Overview

The qcheck-stm plugin for ortac (called Ortac/QCheck-STM in order to avoid ambiguities) generates a standalone executable using QCheck-STM to perform model-based state-machine testing of a module, building up the model from its Gospel specifications.

In order to be able to generate the STM module, the plugin will need five pieces of information:

1. What type do we want to test? This is called system under test or SUT by QCheck-STM.
2. How to generate a value of this type? The init_sut function.
3. What is the model of this type? This is what is taken as the state by QCheck-STM.
4. How to generate the said model? The init_state function.
5. How does the model change when calling a function? The next_state function.

Answering these five questions is done part in the command-line arguments and part in the Gospel specifications that you will have to write in a specific style.

This tutorial aims at showing how to write Gospel specifications for your modules in order to be able to automatically generate the QCheck-STM tests with the ortac command-line tool and its Ortac/QCheck-STM plugin.

We are going to build an example for a simple fixed-size container library.

How to write Gospel specifications?

In order to use the Ortac/QCheck-STM, the module you want to test must contain three kinds of items:

1. The type declaration for SUT
2. The function used to generate the initial value of SUT
3. Functions to be tested

Here is an example for the declaration of type SUT:

type 'a t
(*@ model size : int
    mutable model contents : 'a list *)

You'll notice the Gospel specifications under the type declaration, in the special Gospel comments. These specifications give two models to the type, one non mutable and one mutable. These models are necessary (or at least some models) in order to give enough information to the qcheck-stm plugin to build the functional state that QCheck-STM will be using. This item is then bringing two needed pieces of information: what are the type of the SUT and the type of the state.

The second item is the function used for generating the inital value for SUT. Here again, this item will bring two needed pieces of information: how to build the initial value of SUT and the corresponding state. This is the role of the make function along with its specification.

val make : int -> 'a -> 'a t
(*@ t = make i a
    checks i >= 0
    ensures t.size = i
    ensures t.contents = List.init i (fun j -> a) *)

Obviously, the function should return a value of type SUT. But more importantly, the specification has to give a value to each of the models that were given to the type SUT in its specification. Here, this means we need to give a value to t.size and to t.contents. The checks clause is part of the Gospel specification of the function, but it won't be used by the plugin to generate any code. You can give more information that the plugin needs, for example if you are also using another tool based on Gospel specifications. The plugin will simply ignore them.

Now that Ortac/QCheck-STM is able to generate an initial value for the type under test and its model, we can turn our attention to the functions we will want to test. Here is the example of the classic set function along with its Gospel specification written with the qcheck-stm ortac plugin in mind:

val set : 'a t -> int -> 'a -> unit
(*@ set t i a
    checks 0 <= i < t.size
    modifies t.contents
    ensures t.contents = List.mapi (fun j x -> if j = (i : integer) then a else x) (old t.contents) *)

The most important purpose of the specifications (in the context of this tutorial) is to bring the last piece of information. That is to answer the question about how the model changes when calling the specified function. This is done in two steps.

First, you have to declare which of the model's field are modified in the modifies clause. Note that if, like in the case of the set function, the function is returning unit, it is a Gospel error to not give any modifies clause. But Gospel lets you write modifies () in order to express the fact that the function is modifying something that is not in the model of any of the argument. However, Ortac/QCheck-STM will read the modifies clauses (if any) in order to determine which model's fields are modified when the function is called. The model's fields that don't appear in any of the modifies clauses will be considered as not modified.

Then, the plugin will look at the ensures clauses (the postconditions) in order to find one clause per modified field that expresses how to compute the modification. For now, the tool is not very smart. The basic rule of thumb is that you need to write down a computable description of the new model's field as a function of the old one. This will often mean that you need to write stronger postconditions that what would be necessary in another context. If the plugin can't find any suitable ensures clause, it will raise a warning and skip the function for test.

You can see again the checks clause. This time, as the function is a candidate for test, the checks clause will be used by the tool to check that if the condition of the clause is not respected, the function raises the Invalid_arg exception.

Now that the set function is ready to be tested, let's turn our attention to another example. Here is the example of the get function along with its Gospel specifications:

val get : 'a t -> int -> 'a
(*@ a = get t i
    checks 0 <= i < t.size
    ensures a = List.nth t.contents i *)

Here, the ensures clause has another use. As the get function does not modifies anything, there is no need to give the values of the model’s fields after the function. Note that the ensures clause wouldn't have been fit for this purpose anyway. The ensures clauses that are not used for the next_state function are used for checking postconditions, here a postcondition stating a relation between the returned value and the function arguments. These ensures clauses are not necessary to generate the QCheck-STM tests, but they will bring strength to your tests.

In order to generate postcondition-checking, Ortac/QCheck-STM uses the ensures clauses that were not used for the next_state function but it also uses the checks clauses and the raises ones.

Now you can generate the QCheck-STM file by running the following command where you indicate the file you want to test, the function call to build a value of the type indicated in the third argument. You can write the generated code into a file, using the -o option.

$ ortac qcheck-stm example.mli "make 42 'a'" "char t" -o stm_example.ml

The generated OCaml file has a bunch of dependencies:

• qcheck-core
• qcheck-core.runner
• qcheck-stm.stm
• qcheck-stm.sequential
• qckeck-multicoretests-util
• ortac-runtime

Using the dune build system, your dune rule for the example above would look like the following:

(test
 (name stm_example)
 (libraries
  qcheck-core
  qcheck-core.runner
  qcheck-stm.stm
  qcheck-stm.sequential
  qcheck-multicoretests-util
  ortac-runtime
  example)
 (action
  (run %{test} --verbose)))

Warning system

Now that you know what Gospel specifications for the qcheck-stm plugin should look like and how to generate the QCheck-STM file, let's focus on what can go wrong. The qcheck-stm plugin has an extensive set of warnings to help you formulate your specifications in a way it can use.

Most of the time, Ortac/QCheck-STM will skip a function if it can't generate one of the elements needed by QCheck-STM. Doing so, it will display a warning on stderr in order for you to be able to get an idea about test coverage.

Ortac/QCheck-STM specifics

Let's start with the warnings specific to the plugin.

The principle at the core of Ortac/QCheck-STM is to turn the Gospel specifications into OCaml code needed by the QCheck-STM test framework. This means that you need to provide these pieces of information into the specification in a style that allows the plugin to understand them.

The most delicate piece of information you have to give is how the function modifies the model of the SUT. As stated above, the plugin is looking for this information in the ensures clauses.

If Ortac/QCheck-STM doesn't have enough information in your specifications in order to compute the next value for every model's field appearing in a modifies clause, it won't be able to test the function and inform you with a warning.

For example, the following specifications are not enough for Ortac/QCheck-STM.

val ensures_not_found_for_next_state : 'a t -> unit
(*@ ensures_not_found_for_next_state t
    modifies t.contents
    ensures List.length t.contents = List.length (old t.contents) *)

Ortac/QCheck-STM will look at the modifies clause and then look for an ensures clause for each of the modified models that allows to compute its new value. Here, it won't find any and warn you with the following message:

$ ortac qcheck-stm example_next_state.mli "make 42 'a'" "char t" -o foo.ml
File "example_next_state.mli", line 15, characters 13-23:
15 |     modifies t.contents
                  ^^^^^^^^^^
Warning: Skipping ensures_not_found_for_next_state: model contents is
         declared as modified by the function but no suitable ensures clause
         was found. Specifications should contain at least one "ensures
         x.contents = ..." where x is the SUT.

Note that you don't have to rewrite the clause. Maybe it contains information you still want to state in your specifications. You can then add another ensures clause with the relevant information in order to compute the new value of the modified model. The warning message gives you the form in which the plugin expects to find the information, namely a description of the new state by an expression in which any reference to the state should be to the old state (that is the state before the function is called).

Note also that if you write modifies t, the plugin assumes that all the mutable fields are modified and will try to find a description for all of them. So you'll need to avoid being too general in the modifies clauses.

Internally, QCheck-STM uses an extensible type to encode function's type signature. The plugin uses the type signature to automatically generate this encoding. But, in case you are using a type that is not yet encoded in this extensible type, Ortac/QCheck-STM will generate code using the not-yet-defined constructor using the implicit rule of capitalizing the name of the type. This will generate non-compiling code, but you'll then have the chance to add the new constructor by hand in the generated code.

For example, looking at the following function along its specifications, the plugin will make the assumption that the QCheck-STM `ty` is extended with a New_type constructor and a new_type functional combinator is defined.

val type_not_supported : new_type -> 'a t -> new_type
(*@ y = type_not_supported x t *)

$ ortac qcheck-stm example_unknown_type.mli "make 42 'a'" "char t" -o foo.ml
$ grep -A 1 "type cmd" foo.ml
    type cmd =
      | Type_not_supported of new_type
$ grep -A 3 "let run" foo.ml
    let run cmd__010_ sut__011_ =
      match cmd__010_ with
      | Type_not_supported x ->
          Res (new_type, (type_not_supported x sut__011_))

You can open the foo.ml file to edit it in this way.

In Gospel, you have the possibility to use ghost values, as arguments and/or as returned values. As those values don’t exist in the actual code that will be called during the test, Ortac/QCheck-STM doesn't support Gospel specifications with ghost values in the header.

If we add the following declaration to our example file,

val ghost_arg : char -> 'a t -> bool
(*@ b = ghost_arg [ i : integer] c t *)

the command will generate the following warning:

$ ortac qcheck-stm example_ghost.mli "make 42 'a'" "char t" -o foo.ml
File "example_ghost.mli", line 14, characters 20-21:
14 | (*@ b = ghost_arg [ i : integer] c t *)
                         ^
Warning: Skipping ghost_arg: functions with a ghost argument are not
         supported.

You'll need to write your specifications without using ghost arguments or returned value if you want to test this function with Ortac/QCheck-STM.

Finally, when you want to test a library with a parameterized type, you need to instantiate the type parameter in order to generate the QCheck-STM tests. Choosing the right instantiation implies to be careful when the library contains specialized functions.

For example, if we add the following declaration to our example file,

val incompatible_type : char -> string t -> bool
(*@ b = incompatible_type c t *)

the plugin will generate a warning for this function and skip it.

$ ortac qcheck-stm example_incompatible_type.mli "make 42 'a'" "char t" -o foo.ml
File "example_incompatible_type.mli", line 13, characters 32-40:
13 | val incompatible_type : char -> string t -> bool
                                     ^^^^^^^^
Warning: Skipping incompatible_type: the type of its SUT-type argument is
         incompatible with the configured SUT type: char t.

In the case you have functions specialized with different instantiations, you can always generate one test per possible instantiation, of course.

ortac limitations

The second source of limitations is the ocaml_of_gospel translation provided by the ortac-core package. Gospel being a logical language, it is not fully executable. ortac-core identifies an executable subset of Gospel and translates it to OCaml. But there are still some limitations, in particular concerning quantification. For now, only well-bounded quantifications over integers are supported.

If we add the following declaration to our example file,

val unsupported_quantification : 'a t -> bool
(*@ b = unsupported_quantification t
    ensures b = forall a. List.mem a t.contents -> a = a *)

the command will generate the following warning:

$ ortac qcheck-stm example_ill_formed_quantification.mli "make 42 'a'" "char t" -o foo.ml
File "example_ill_formed_quantification.mli", line 15, characters 16-56:
15 |     ensures b = forall a. List.mem a t.contents -> a = a *)
                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning: Skipping clause: unsupported quantification.

Note that only the clause involving the unsupported quantification has not been translated. If your function's specification contains other clauses that can be translated and contain enough information for the plugin to do its job, then you will be able to test your function. If not, maybe you can rewrite the clause without involving this sort of quantification. In this particular example, you can use the List.for_all combinator from the Gospel standard library List module:

val for_all : 'a t -> bool
(*@ b = for_all t
    ensures b = List.for_all (fun x -> x = x) t.contents *)

Other limitations

Finally, note that this tool is still fairly new and comes with limitations that should be lifted in the future. Fow now, we only support testing functions with exactly one SUT argument in its signature, we don't support tuples and we only support first-order functions.

If we add the following declarations to our example file,

val f : int -> int -> bool
(*@ b = f x y *)

val compare : 'a t -> 'a t -> bool
(*@ b = compare t1 t2 *)

val of_list : 'a list -> 'a t
(*@ t = of_list xs *)

val g : int * int -> 'a t -> bool
(*@ b = g x t *)

val h : 'a t -> 'a * 'a
(*@ (l, r) = h t *)

val for_all : ('a -> bool) -> 'a t -> bool
(*@ b = for_all p t *)

Ortac/QCheck-STM will generate the following warnings:

$ ortac qcheck-stm example_limitations.mli "make 42 'a'" "char t" -o foo.ml
File "example_limitations.mli", line 13, characters 8-26:
13 | val f : int -> int -> bool
             ^^^^^^^^^^^^^^^^^^
Warning: Skipping f: functions with no SUT argument cannot be tested.
File "example_limitations.mli", line 16, characters 14-34:
16 | val compare : 'a t -> 'a t -> bool
                   ^^^^^^^^^^^^^^^^^^^^
Warning: Skipping compare: functions with multiple SUT arguments cannot be
         tested.
File "example_limitations.mli", line 19, characters 25-29:
19 | val of_list : 'a list -> 'a t
                              ^^^^
Warning: Skipping of_list: functions returning a SUT value cannot be tested.
File "example_limitations.mli", line 25, characters 16-23:
25 | val h : 'a t -> 'a * 'a
                     ^^^^^^^
Warning: Skipping h: functions returning tuples are not supported yet.
File "example_limitations.mli", line 28, characters 15-25:
28 | val for_all : ('a -> bool) -> 'a t -> bool
                    ^^^^^^^^^^
Warning: Skipping for_all: functions are not supported yet as arguments.
File "example_limitations.mli", line 22, characters 8-17:
22 | val g : int * int -> 'a t -> bool
             ^^^^^^^^^
Warning: Type (int * int) not supported.