QuickChick : forAll and forAllShrink for binary functions

Using Coq
1

Hello,

Is there any analogues of forAll and forAllShrink property combinators,
to test property, which expects 2 arguments.

I am not sure, but maybe it will look like this:

QuickChick (forAllShrink2 
                         some_generator_1
                         some_generator_2
                         shrink_1
                         shrink_2
                         binary_function_my_property
           ).

I managed to write such a function for forAll :

Definition forAll2 {A B C: Type} `{Show A} `{Show C} `{Checkable B}
                  (g1 : G A) (g2 : G C) (f : A -> C -> B)
                : Checker :=
  a <- g1 ;;
  c <- g2 ;;  
  r <- checker (f a c) ;;
  match r with
    Success => ret Success
  | Failure b => ret (Failure (a,c,b))
  end.

but I didn’t write same for forAllShrink, so maybe I am reinventing the wheel, and such property combinators already exists. Please advice.

Thanks.

1 Like
2

I’d recommend uncurrying the property function:

From QuickChick Require Import QuickChick.

Parameters A B C: Type.
Parameter some_generator_1: G A.
Parameter some_generator_2: G C.
Parameter shrink_1: A -> list A.
Parameter shrink_2: C -> list C.
Parameter binary_function_my_property: A -> C -> B.

Instance Gen__A : Gen A := Build_Gen _ some_generator_1.
Instance Gen__C : Gen C := Build_Gen _ some_generator_2.
Instance Gen__AC: Gen (A * C) := Instances.genPair.

Instance Shrink__A : Shrink A := Build_Shrink _ shrink_1.
Instance Shrink__C : Shrink C := Build_Shrink _ shrink_2.
Instance Shrink__AC: Shrink (A * C) := shrinkPair.

Check (forAllShrink arbitrary shrink (uncurry binary_function_my_property)).
1 Like