Module `Ppx_pbt`

Ppx for property-based test generation

This library intends to facilitate the writing of property-based test. The main purpose is to easily test redundant properties on multiple functions, a level of abstraction of property-based testing libraries is offered using properties and generators through identifiers.

Example:

Addition is commutative:

let add = (+) [@@pbt "commutative[int, int]"]

(* ==> *)
include struct
  let add = (+)

  let test_add_is_commutative =
    QCheck.Test.make
      ~name:"add_is_commutative"
      (QCheck.pair QCheck.int QCheck.int)
      (fun (arb_0, arb_1) -> Pbt.Properties.commutative add arb_0 arb_1)

  let () = Runner.add_tests [ test_add_is_commutative ]
end

Annotation-based system

Annotation language

<properties> ::= <property list>
<property> ::= <ident> <args> <gens>
<args> ::= { <ident list> }
<gens> ::= [ <ident list> ]

The property is splitted between 3 sub-components:

property name
arguments names (can be empty)
generators names (can be empty)

Example without arguments:

let add = (+) [@@pbt "commutative[int, int]"]

property name: commutative
arguments names: none
generators names: int, int

Example with arguments:

let zero = 0
let add = (+) [@@pbt "absorbs{zero}[int]"]

property name: absorbs
arguments names: zero
generators names: int

Specifying generators

Generators are created using ppx_deriving_qcheck. They are for now a QCheck arbitrary, but for clarity we use the word generator (i.e arbitrary will be removed when QCheck2 is released).

see https://github.com/vch9/ppx_deriving_qcheck

There can be 2 ways to specify generators in annotations:

Specify your own generators If you want to provide your own generators, you must introduced a QCheck arbitrary named arb_[name].

Example:

(** unsigned int *)
type uint = int

let arb_uint = QCheck.(map abs int)

let add = (+) [@@pbt "commutative[arb_uint, arb_uint]"]

Use ppx_deriving_qcheck Ppx_deriving_qcheck supports multiple primitive types, but if it fails to create a QCheck arbitrary for a given arbitrary, a arb_[type_name] will be created

Example:

let add = (+) [@@pbt "commutative[uint, int]"]

(* => *)
include struct
  let add = (+)

  let test_add_is_commutative =
    QCheck.Test.make
      ~name:"add_is_commutative"
      (QCheck.pair QCheck.arb_uint QCheck.int) (* <- see here *) 
      (fun (arb_0, arb_1) -> Pbt.Properties.commutative add arb_0 arb_1)

  let () = Runner.add_tests [ test_add_is_commutative ]
end

Specifying properties

Properties must be used with an identifier, a list of properties can be found at Pbt.Properties.

If it fails to find a properties inside Pbt.Properties, a local function describing a property must be found in the local scope.

Example:

 let arb_set = QCheck.(list int)

 (** [get_and_set f s x y] tests
     mem [s] [x] ==> mem ([f] [s] [x] [y]) [y] *)

 let get_and_set f s x y =
   not (List.mem s x) || List.mem (f s x y) y

 (** [find_and_replace s x y] replaces [x] by [y] in [s] *)
 let find_and_replace s x y = ...
   [@@pbt "get_and_set[arb_set, int, int]"]

 (** => *)

 let arb_set = QCheck.(list int)

 (** [get_and_set f s x y] tests
     mem [s] [x] ==> mem ([f] [s] [x] [y]) [y] *)

 let get_and_set f s x y =
   not (List.mem x s) || List.mem y (f s x y) 

 include struct
   (** [find_and_replace s x y] replaces [x] by [y] in [s] *)
   let find_and_replace s x y = ...
     [@@pbt "get_and_set[arb_set, int, int]"]

   let test_find_and_replace_is_get_and_set =
     QCheck.Test.make ~name:"find_and_replace_is_get_and_set"
       (QCheck.pair arb_set (QCheck.pair QCheck.int QCheck.int))
       (fun (arb_0, (arb_1, arb_2)) ->
          get_and_set find_and_replace arb_0 arb_1 arb_2)

   let () = Runner.add_tests [test_find_and_replace_is_get_and_set]
end

Annotations in implementation files

Properties can be directly attached with attributes inside function implementation. The test will be inlined directly after the function under test.

Example:

let add = (+) [@@pbt "commutative[int, int]"]

(* ==> *)
include struct
  let add = (+)

  let test_add_is_commutative =
    QCheck.Test.make
      ~name:"add_is_commutative"
      (QCheck.pair QCheck.int QCheck.int)
      (fun (arb_0, arb_1) -> Pbt.Properties.commutative add arb_0 arb_1)

  let () = Runner.add_tests [ test_add_is_commutative ]
end

Annotations in interface files

Properties can also be attached to function declaration in interface files. Having annotation in signature allows the possibility to infer required generators for a function declaration.

ppx_deriving_qcheck is used to automatically infer generators when it's possible.

see https://github.com/vch9/ppx_deriving_qcheck

Example:

(* foo.mli *)
val add : int -> int -> int [@@pbt "commutative"]

(* foo.ml *)
include struct
  let add = (+)

  let test_add_is_commutative =
    QCheck.Test.make
      ~name:"add_is_commutative"
      (QCheck.pair QCheck.int QCheck.int)
      (fun (arb_0, arb_1) -> Pbt.Properties.commutative add arb_0 arb_1)

  let () = Runner.add_tests [ test_add_is_commutative ]
end

However, annotations are only allowed in signatures outside any structure item and inside only modules and functors at the moment.

Alcotest runner

class mapper : object ... end