Skip to content

Latest commit

 

History

History
145 lines (104 loc) · 4.26 KB

README.md

File metadata and controls

145 lines (104 loc) · 4.26 KB
Raw

QCheck-STM plugin for Ortac

This directory contains a plugin for Ortac that can generate a standalone executable using QCheck-STM to perform model-based state-machine testing of a module by using the model of its Gospel specifications.

Installation

Follow the global installation instructions in the main README of this repository. The QCheck-STM plugin is provided by the ortac-qcheck-stm OPAM package, which depends on the ortac-core and ortac-runtime packages.

Quick start

The QCheck-STM plugin can be used to generate a program using the QCheck-STM library to test the consistency between the actual behaviours of the functions of a module and their expected behaviours as specified by their Gospel model.

Let’s start with a module lib.mli defining a (array-like) data structure containing some Gospel specifications:

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

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) *)

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

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) *)

To generate a QCheck-STM test program for that library, you must indicate:

  • the type of the system under test, for instance char t, where the type t must have a Gospel model that will be used as the model state by the QCheck-STM library,
  • how to generate an initial value of that type, for instance make 16 'a'.

You can do so with the following lib_conf.ml file:

open Lib
type sut = char t
let init_sut = make 16 'a'

You can then run:

$ ortac qcheck-stm lib.mli lib_conf.ml

to generate the corresponding QCheck-STM program. The QCheck-STM documentation explains the structure of a specification such as the one that is generated by the plugin.

You can then save this module into a file:

$ ortac qcheck-stm lib.mli lib_conf.ml -o main.ml

and compile this into an executable using:

  • the library Lib itself, obviously,
  • the libraries qcheck-core, qcheck-stm.sequential and ortac-runtime.

With dune, the configuration would then look something like:

(executable
 (name main)
 (libraries lib qcheck-core qcheck-stm.sequential ortac-runtime))

From there, you can run the program directly for random testing:

$ ./path/to/main.exe

Using the dune-rules plugin

When using the QCheck-STM plugin in a testing setup the creation of the required dune files can be automated with the dune-rules plugin. See the dedicated README for details.

Supported Gospel and other limitations

The QCheck-STM plugin currently has some limitations on what Gospel specifications are supported.

First of all it inherits the limitations of the translation from Gospel to OCaml provided by the core of Ortac, as listed in the main README.

At the moment, the plugin also comes with the following limitations:

  • every argument of the functions that will be tested will be generated using the generator of QCheck.Gen whose name matches the type of that argument,
  • when a function modifies the model state, it must come with a specification ensures t.field = expr for every field that is modified, where expr must be computable with only the old state,
  • the specification of the function that is used to generate the initial value of the system under test (make in the small example above) must come with a specification ensures t.field = ... for every field of the model so that the initial state can be computed.

Acknowledgment

This plugin is based on an early proof of concept written by Naomi Spargo.