CODEWITHSUNDEEP
testingocamlproperty-based-testing
haochenx
haochenx

Reputation: 163

Can QCheck (OCaml property-based testing library) be used to perform exhaustive testing?

Regarding the OCaml QCheck library (https://github.com/c-cube/qcheck), say we have a complete generator g: typ Gen.t for a finite type typ or a finite subset s: typ -> bool of typ, is it possible (with or without resorting to hacky techniques and/or slight modification to the library itself) to perform an exhaustive test (thus a proof!) for a property e.g. forall x (s.t. s x = true in the case we are only interested in a subset), prop x = true, given prop: typ -> bool always return a value for either any value of the type or the subset we are interested in?

By a "complete generator", I don't have a concrete definition for it but something as the name suggests. Some examples include:

Upvotes: 2

Views: 106

Answers (1)

octachron
octachron

Reputation: 18902

In brief, this is possible but it is really unclear if it is desirable.

Indeed, you can define a qcheck generator from an exhaustive sequence

let make_gen seq =
  let current = ref seq in
  let rec gen state = match !current () with
    | Seq.Cons (x,seq) ->
      current := seq;
      x
    | Seq.Nil ->
      current := seq;
      gen state
  in
  let shrink _x () = Seq.Nil in
  QCheck2.Gen.make_primitive ~gen ~shrink

and use Qcheck runner to test properties on the total number of elements in this existing sequence.

However, it is then not clear what Qcheck brings you since you can not use any of the other Qcheck generators: even for a finite set, a random generator will require an infinite number of samples to almost surely cover all cases. Similarly, for an exhaustive generator, shrinking is not useful since you will have to test all values at some point.

Upvotes: 0

Related Questions