Stream: Coq users

Topic: QuickChick - discard-friendly conjoin?

Mikkel Milo (Aug 26 2020 at 07:26):

QuickChick's conjoin results in a discarded test if at least one of the given list of checkers is discarded (and none fail), but would it be possible to implement a variant that evaluates to success even in the presence of discards? i.e (conjoin' [false ==> true; checker true]) would result in success, and not a discard.

Li-yao (Aug 26 2020 at 13:28):

that seems possible. maybe a simpler thing to do is a combinator to mark discards as successes? Don't hesitate to open an issue on the repository.

Mikkel Milo (Aug 27 2020 at 08:37):

Li-yao said:

maybe a simpler thing to do is a combinator to mark discards as successes?

That does indeed sound much simpler. I'm not too familiar with the inner workings of QuickChick, but after looking at https://github.com/QuickChick/QuickChick/blob/8.12/src/Checker.v I think I was able to derive a combinator which does exactly this:

Definition discardToSuccess {prop} `{Checkable prop} (p : prop): Checker :=
  mapTotalResult (fun res => match res.(ok) with
                             | None => updOk res (Some true)
                             | _ => res
                             end) p.

QuickChick (discardToSuccess (false ==> true)).
(* +++ Passed 10000 tests (0 discards) *)
QuickChick (discardToSuccess true).
(* +++ Passed 10000 tests (0 discards) *)
QuickChick (discardToSuccess false).
(* *** Failed after 1 tests and 0 shrinks. (0 discards) *)

Seems like it works as intended since false ==> true is tested with success now instead of being discarded. Thanks for the suggestion!

Last updated: Oct 03 2023 at 04:02 UTC