Skip to content

Draft: Property-based testing with Tezt

François Thiré requested to merge francois@pbt into master

⚠ This is WIP work ⚠

Description / Motivation

This MR introduces a property-based testing engine to be used with Tezt.

The main features are:

  • Features integrated shrinking: When a counter-example is found, it tries to find a hopefully smaller counter-example.
  • Features internal shrinking: Counter-example are actually smaller (this is not true with integrated shrinking)
  • Minimal kernel: All the logic lies in less than 200 hundred lines of OCaml code (tree.ml and gen.ml)
  • Predictability: The default behaviour is easy to understand. Hence it is easy to predict what it is doing
  • Extensibility: The default behaviour of the shrinker can be modified to integrate better strategies without jeopardizing the correction of the shrinker
  • UX friendly: We reuse the Tezt engine to create a friendly UX for this framework:
    • While debugging a test, capture stderr except for the minimal example found by the shrinker
    • (TODO) Because there is no one strategy but multiple strategies, we could accelerate the search of a counter-example using -j x option of Tezt

I will document later how it works and also provide more default generators. However, with the current MR, many of the generators could be defined using the engine. For example:

let bool = 
   let open Gen.Syntax in
let* x = Gen.range 0 1 in if x = 0 then return false else return true

let char = 
   let open Gen.Syntax in
   Gen.range 0 25 in Char.chr (Char.code 'a' + x)

let string ~size = 
   let open Gen.Syntax in
   Std.list ~size char

The nice property is that the shrinker we get this way is very predictable once we know how the library is made. The shrinker for string, for example will shrink towards a prefix of the string and, for each character, shrink towards the letter 'a'. If the string "aefu" was generated, you can be sure that all counter-example will have the following property: 1) the first character is 'a' 2) The second character is between "a" and "e",3) the third character is "f" 4) the fourth character is between "a" and "u".

The library already offers default tactics. For example with the Suffix tactic, instead of shrinking towards the prefix, it shrinks towards the suffix (example : "aefg" may produce ["efg";"f";"g"; ""]). With the Skip tactic, the shrinker may remove some characters. If we use Skip 1, one character is removed. So going from our example above "aefg", the shrinker may try first the list of strings ["afg";"efg";"afe";"afg"].

Merge request reports