mirror of
https://github.com/c-cube/ocaml-containers.git
synced 2025-12-06 11:15:31 -05:00
updated QCheck
This commit is contained in:
parent
b9d38ff624
commit
82c1ded882
2 changed files with 108 additions and 43 deletions
100
qCheck.ml
100
qCheck.ml
|
|
@ -43,6 +43,12 @@ module Arbitrary = struct
|
||||||
|
|
||||||
let small_int = int 100
|
let small_int = int 100
|
||||||
|
|
||||||
|
let split_int gen st =
|
||||||
|
let n = gen st in
|
||||||
|
if n > 0
|
||||||
|
then let i = Random.State.int st (n+1) in i, n-i
|
||||||
|
else 0, 0
|
||||||
|
|
||||||
let bool = Random.State.bool
|
let bool = Random.State.bool
|
||||||
|
|
||||||
let float f st = Random.State.float st f
|
let float f st = Random.State.float st f
|
||||||
|
|
@ -90,24 +96,26 @@ module Arbitrary = struct
|
||||||
Array.init n (fun _ -> ar st)
|
Array.init n (fun _ -> ar st)
|
||||||
|
|
||||||
let among_array a st =
|
let among_array a st =
|
||||||
|
if Array.length a < 1
|
||||||
|
then failwith "Arbitrary.among: cannot choose in empty array ";
|
||||||
let i = Random.State.int st (Array.length a) in
|
let i = Random.State.int st (Array.length a) in
|
||||||
a.(i)
|
a.(i)
|
||||||
|
|
||||||
let among l = among_array (Array.of_list l)
|
let among l =
|
||||||
|
if List.length l < 1
|
||||||
|
then failwith "Arbitrary.among: cannot choose in empty list";
|
||||||
|
among_array (Array.of_list l)
|
||||||
|
|
||||||
let choose l =
|
let choose l = match l with
|
||||||
assert (l <> []);
|
| [] -> failwith "cannot choose from empty list"
|
||||||
let a = Array.of_list l in
|
| [x] -> x
|
||||||
fun st ->
|
| _ ->
|
||||||
let i = Random.State.int st (Array.length a) in
|
let a = Array.of_list l in
|
||||||
a.(i) st
|
fun st ->
|
||||||
|
let i = Random.State.int st (Array.length a) in
|
||||||
|
a.(i) st
|
||||||
|
|
||||||
let _fix ~max ~depth recursive f =
|
let fix ?(max=15) ~base f =
|
||||||
let rec ar = lazy (fun st -> (Lazy.force ar_rec) st)
|
|
||||||
and ar_rec = lazy (f ar) in
|
|
||||||
Lazy.force ar
|
|
||||||
|
|
||||||
let fix ?(max=max_int) ~base f =
|
|
||||||
let rec ar = lazy
|
let rec ar = lazy
|
||||||
(fun depth st ->
|
(fun depth st ->
|
||||||
if depth >= max || Random.State.int st max < depth
|
if depth >= max || Random.State.int st max < depth
|
||||||
|
|
@ -122,6 +130,10 @@ module Arbitrary = struct
|
||||||
let max = depth st in
|
let max = depth st in
|
||||||
fix ~max ~base f st
|
fix ~max ~base f st
|
||||||
|
|
||||||
|
let rec retry gen st = match gen st with
|
||||||
|
| None -> retry gen st
|
||||||
|
| Some x -> x
|
||||||
|
|
||||||
let lift f a st = f (a st)
|
let lift f a st = f (a st)
|
||||||
|
|
||||||
let lift2 f a b st = f (a st) (b st)
|
let lift2 f a b st = f (a st) (b st)
|
||||||
|
|
@ -169,22 +181,22 @@ module PP = struct
|
||||||
|
|
||||||
let list pp l =
|
let list pp l =
|
||||||
let b = Buffer.create 25 in
|
let b = Buffer.create 25 in
|
||||||
Buffer.add_char b '(';
|
Buffer.add_char b '[';
|
||||||
List.iteri (fun i x ->
|
List.iteri (fun i x ->
|
||||||
if i > 0 then Buffer.add_string b ", ";
|
if i > 0 then Buffer.add_string b ", ";
|
||||||
Buffer.add_string b (pp x))
|
Buffer.add_string b (pp x))
|
||||||
l;
|
l;
|
||||||
Buffer.add_char b ')';
|
Buffer.add_char b ']';
|
||||||
Buffer.contents b
|
Buffer.contents b
|
||||||
|
|
||||||
let array pp a =
|
let array pp a =
|
||||||
let b = Buffer.create 25 in
|
let b = Buffer.create 25 in
|
||||||
Buffer.add_char b '[';
|
Buffer.add_string b "[|";
|
||||||
Array.iteri (fun i x ->
|
Array.iteri (fun i x ->
|
||||||
if i > 0 then Buffer.add_string b ", ";
|
if i > 0 then Buffer.add_string b ", ";
|
||||||
Buffer.add_string b (pp x))
|
Buffer.add_string b (pp x))
|
||||||
a;
|
a;
|
||||||
Buffer.add_char b ']';
|
Buffer.add_string b "|]";
|
||||||
Buffer.contents b
|
Buffer.contents b
|
||||||
end
|
end
|
||||||
|
|
||||||
|
|
@ -216,7 +228,7 @@ end
|
||||||
type 'a result =
|
type 'a result =
|
||||||
| Ok of int * int (* total number / precond failed *)
|
| Ok of int * int (* total number / precond failed *)
|
||||||
| Failed of 'a list
|
| Failed of 'a list
|
||||||
| Error of exn
|
| Error of 'a option * exn
|
||||||
|
|
||||||
(* random seed, for repeatability of tests *)
|
(* random seed, for repeatability of tests *)
|
||||||
let __seed = [| 89809344; 994326685; 290180182 |]
|
let __seed = [| 89809344; 994326685; 290180182 |]
|
||||||
|
|
@ -224,9 +236,11 @@ let __seed = [| 89809344; 994326685; 290180182 |]
|
||||||
let check ?(rand=Random.State.make __seed) ?(n=100) gen prop =
|
let check ?(rand=Random.State.make __seed) ?(n=100) gen prop =
|
||||||
let precond_failed = ref 0 in
|
let precond_failed = ref 0 in
|
||||||
let failures = ref [] in
|
let failures = ref [] in
|
||||||
|
let inst = ref None in
|
||||||
try
|
try
|
||||||
for i = 0 to n - 1 do
|
for i = 0 to n - 1 do
|
||||||
let x = gen rand in
|
let x = gen rand in
|
||||||
|
inst := Some x;
|
||||||
try
|
try
|
||||||
if not (prop x)
|
if not (prop x)
|
||||||
then failures := x :: !failures
|
then failures := x :: !failures
|
||||||
|
|
@ -237,7 +251,7 @@ let check ?(rand=Random.State.make __seed) ?(n=100) gen prop =
|
||||||
| [] -> Ok (n, !precond_failed)
|
| [] -> Ok (n, !precond_failed)
|
||||||
| _ -> Failed (!failures)
|
| _ -> Failed (!failures)
|
||||||
with e ->
|
with e ->
|
||||||
Error e
|
Error (!inst, e)
|
||||||
|
|
||||||
(** {2 Main} *)
|
(** {2 Main} *)
|
||||||
|
|
||||||
|
|
@ -247,13 +261,23 @@ type 'a test_cell = {
|
||||||
prop : 'a Prop.t;
|
prop : 'a Prop.t;
|
||||||
gen : 'a Arbitrary.t;
|
gen : 'a Arbitrary.t;
|
||||||
name : string;
|
name : string;
|
||||||
|
limit : int;
|
||||||
|
size : ('a -> int) option;
|
||||||
}
|
}
|
||||||
type test =
|
type test =
|
||||||
| Test : 'a test_cell -> test
|
| Test : 'a test_cell -> test
|
||||||
(** GADT needed for the existential type *)
|
(** GADT needed for the existential type *)
|
||||||
|
|
||||||
let mk_test ?(n=100) ?pp ?(name="<anon prop>") gen prop =
|
let mk_test ?(n=100) ?pp ?(name="<anon prop>") ?size ?(limit=10) gen prop =
|
||||||
Test { prop; gen; name; n; pp; }
|
if limit < 0 then failwith "QCheck: limit needs be >= 0";
|
||||||
|
if n <= 0 then failwith "QCheck: n needs be >= 0";
|
||||||
|
Test { prop; gen; name; n; pp; size; limit; }
|
||||||
|
|
||||||
|
(* tail call version of take, that returns (at most) [n] elements of [l] *)
|
||||||
|
let rec _list_take acc l n = match l, n with
|
||||||
|
| _, 0
|
||||||
|
| [], _ -> List.rev acc
|
||||||
|
| x::l', _ -> _list_take (x::acc) l' (n-1)
|
||||||
|
|
||||||
let run ?(out=stdout) ?(rand=Random.State.make __seed) (Test test) =
|
let run ?(out=stdout) ?(rand=Random.State.make __seed) (Test test) =
|
||||||
Printf.fprintf out "testing property %s...\n" test.name;
|
Printf.fprintf out "testing property %s...\n" test.name;
|
||||||
|
|
@ -263,16 +287,35 @@ let run ?(out=stdout) ?(rand=Random.State.make __seed) (Test test) =
|
||||||
true
|
true
|
||||||
| Failed l ->
|
| Failed l ->
|
||||||
begin match test.pp with
|
begin match test.pp with
|
||||||
| None -> Printf.fprintf out " [×] %d failures\n" (List.length l)
|
| None -> Printf.fprintf out " [×] %d failures over %d\n" (List.length l) test.n
|
||||||
| Some pp ->
|
| Some pp ->
|
||||||
Printf.fprintf out " [×] %d failures:\n" (List.length l);
|
Printf.fprintf out " [×] %d failures over %d (print at most %d):\n"
|
||||||
|
(List.length l) test.n test.limit;
|
||||||
|
let to_print = match test.size with
|
||||||
|
| None -> l
|
||||||
|
| Some size ->
|
||||||
|
(* sort by increasing size *)
|
||||||
|
let l = List.map (fun x -> x, size x) l in
|
||||||
|
let l = List.sort (fun (x,sx) (y,sy) -> sx - sy) l in
|
||||||
|
List.map fst l
|
||||||
|
in
|
||||||
|
(* only keep [limit] counter examples *)
|
||||||
|
let to_print = _list_take [] to_print test.limit in
|
||||||
|
(* print the counter examples *)
|
||||||
List.iter
|
List.iter
|
||||||
(fun x -> Printf.fprintf out " %s\n" (pp x))
|
(fun x -> Printf.fprintf out " %s\n" (pp x))
|
||||||
l
|
to_print
|
||||||
end;
|
end;
|
||||||
false
|
false
|
||||||
| Error e ->
|
| Error (inst, e) ->
|
||||||
Printf.fprintf out " [×] error: %s\n" (Printexc.to_string e);
|
begin match inst, test.pp with
|
||||||
|
| _, None
|
||||||
|
| None, _ -> Printf.fprintf out " [×] error: %s\n" (Printexc.to_string e);
|
||||||
|
| Some x, Some pp ->
|
||||||
|
(* print instance on which the error occurred *)
|
||||||
|
Printf.fprintf out " [×] error on instance %s: %s\n"
|
||||||
|
(pp x) (Printexc.to_string e);
|
||||||
|
end;
|
||||||
false
|
false
|
||||||
|
|
||||||
type suite = test list
|
type suite = test list
|
||||||
|
|
@ -281,11 +324,12 @@ let flatten = List.flatten
|
||||||
|
|
||||||
let run_tests ?(out=stdout) ?(rand=Random.State.make __seed) l =
|
let run_tests ?(out=stdout) ?(rand=Random.State.make __seed) l =
|
||||||
let start = Unix.gettimeofday () in
|
let start = Unix.gettimeofday () in
|
||||||
|
let n = List.length l in
|
||||||
let failed = ref 0 in
|
let failed = ref 0 in
|
||||||
Printf.fprintf out "check %d properties...\n" (List.length l);
|
Printf.fprintf out "check %d properties...\n" (List.length l);
|
||||||
List.iter (fun test -> if not (run ~out ~rand test) then incr failed) l;
|
List.iter (fun test -> if not (run ~out ~rand test) then incr failed) l;
|
||||||
Printf.fprintf out "tests run in %.2fs\n" (Unix.gettimeofday() -. start);
|
Printf.fprintf out "tests run in %.2fs\n" (Unix.gettimeofday() -. start);
|
||||||
if !failed = 0
|
if !failed = 0
|
||||||
then Printf.fprintf out "[✔] Success!\n"
|
then Printf.fprintf out "[✔] Success! (passed %d tests)\n" n
|
||||||
else Printf.fprintf out "[×] Failure (%d tests failed).\n" !failed;
|
else Printf.fprintf out "[×] Failure. (%d tests failed over %d)\n" !failed n;
|
||||||
!failed = 0
|
!failed = 0
|
||||||
|
|
|
||||||
51
qCheck.mli
51
qCheck.mli
|
|
@ -49,14 +49,6 @@ number of instances to generate and test...
|
||||||
|
|
||||||
Examples:
|
Examples:
|
||||||
|
|
||||||
- Not all lists are sorted:
|
|
||||||
|
|
||||||
{[
|
|
||||||
let test = QCheck.(mk_test ~n:10 ~pp:QCheck.PP.(list int)
|
|
||||||
QCheck.Arbitrary.(list small_int) (fun l -> l = List.sort compare l));;
|
|
||||||
QCheck.run test;;
|
|
||||||
]}
|
|
||||||
|
|
||||||
- List.rev is involutive:
|
- List.rev is involutive:
|
||||||
|
|
||||||
{[
|
{[
|
||||||
|
|
@ -64,8 +56,20 @@ let test = QCheck.mk_test ~n:1000 QCheck.Arbitrary.(list alpha)
|
||||||
(fun l -> List.rev (List.rev l) = l);;
|
(fun l -> List.rev (List.rev l) = l);;
|
||||||
QCheck.run test;;
|
QCheck.run test;;
|
||||||
]}
|
]}
|
||||||
|
- Not all lists are sorted (false property that will fail. The 15 smallest
|
||||||
|
counter-example lists will be printed):
|
||||||
|
|
||||||
- generate a tree using {! Arbitrary.fix} :
|
{[
|
||||||
|
let test = QCheck.(
|
||||||
|
mk_test
|
||||||
|
~n:10_000 ~size:List.length ~limit:15 ~pp:QCheck.PP.(list int)
|
||||||
|
QCheck.Arbitrary.(list small_int)
|
||||||
|
(fun l -> l = List.sort compare l));;
|
||||||
|
QCheck.run test;;
|
||||||
|
]}
|
||||||
|
|
||||||
|
|
||||||
|
- generate 20 random trees using {! Arbitrary.fix} :
|
||||||
|
|
||||||
{[type tree = Int of int | Node of tree list;;
|
{[type tree = Int of int | Node of tree list;;
|
||||||
|
|
||||||
|
|
@ -73,7 +77,7 @@ QCheck.run test;;
|
||||||
~base:(map small_int (fun i -> Int i))
|
~base:(map small_int (fun i -> Int i))
|
||||||
(fun t st -> Node (list t st)));;
|
(fun t st -> Node (list t st)));;
|
||||||
|
|
||||||
ar (Random.State.make_self_init ());;
|
Arbitrary.generate ~n:20 ar;;
|
||||||
]}
|
]}
|
||||||
*)
|
*)
|
||||||
|
|
||||||
|
|
@ -92,9 +96,16 @@ module Arbitrary : sig
|
||||||
val int_range : start:int -> stop:int -> int t
|
val int_range : start:int -> stop:int -> int t
|
||||||
(* Integer range start .. stop-1 *)
|
(* Integer range start .. stop-1 *)
|
||||||
|
|
||||||
|
val (--) : int -> int -> int t
|
||||||
|
(** Infix synonym for {!int_range} *)
|
||||||
|
|
||||||
val small_int : int t
|
val small_int : int t
|
||||||
(** Ints lower than 100 *)
|
(** Ints lower than 100 *)
|
||||||
|
|
||||||
|
val split_int : int t -> (int * int) t
|
||||||
|
(** [split_int gen] generates a number [n] from [gen], and
|
||||||
|
returns [i, j] where [i + j = n] *)
|
||||||
|
|
||||||
val bool : bool t
|
val bool : bool t
|
||||||
(** Arbitrary boolean *)
|
(** Arbitrary boolean *)
|
||||||
|
|
||||||
|
|
@ -117,7 +128,7 @@ module Arbitrary : sig
|
||||||
(** Transform an arbitrary into another *)
|
(** Transform an arbitrary into another *)
|
||||||
|
|
||||||
val list : ?len:int t -> 'a t -> 'a list t
|
val list : ?len:int t -> 'a t -> 'a list t
|
||||||
(** List of arbitrary length *)
|
(** List of arbitrary length. Default [len] is between 0 and 10. *)
|
||||||
|
|
||||||
val opt : 'a t -> 'a option t
|
val opt : 'a t -> 'a option t
|
||||||
(** May return a value, or None *)
|
(** May return a value, or None *)
|
||||||
|
|
@ -148,7 +159,7 @@ module Arbitrary : sig
|
||||||
|
|
||||||
val fix : ?max:int -> base:'a t -> ('a t -> 'a t) -> 'a t
|
val fix : ?max:int -> base:'a t -> ('a t -> 'a t) -> 'a t
|
||||||
(** Recursive arbitrary values. The optional value [max] defines
|
(** Recursive arbitrary values. The optional value [max] defines
|
||||||
the maximal depth, if needed. [base] is the base case. *)
|
the maximal depth, if needed (default 15). [base] is the base case. *)
|
||||||
|
|
||||||
val fix_depth : depth:int t -> base:'a t -> ('a t -> 'a t) -> 'a t
|
val fix_depth : depth:int t -> base:'a t -> ('a t -> 'a t) -> 'a t
|
||||||
(** Recursive values of at most given random depth *)
|
(** Recursive values of at most given random depth *)
|
||||||
|
|
@ -161,6 +172,9 @@ module Arbitrary : sig
|
||||||
val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
|
val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
|
||||||
(** Monadic bind *)
|
(** Monadic bind *)
|
||||||
|
|
||||||
|
val retry : 'a option t -> 'a t
|
||||||
|
(** Generate until a Some value is returned *)
|
||||||
|
|
||||||
val generate : ?n:int -> ?rand:Random.State.t -> 'a t -> 'a list
|
val generate : ?n:int -> ?rand:Random.State.t -> 'a t -> 'a list
|
||||||
(** Generate [n] random values of the given type *)
|
(** Generate [n] random values of the given type *)
|
||||||
end
|
end
|
||||||
|
|
@ -213,8 +227,8 @@ end
|
||||||
|
|
||||||
type 'a result =
|
type 'a result =
|
||||||
| Ok of int * int (** total number of tests / number of failed preconditions *)
|
| Ok of int * int (** total number of tests / number of failed preconditions *)
|
||||||
| Failed of 'a list
|
| Failed of 'a list (** Failed instances *)
|
||||||
| Error of exn
|
| Error of 'a option * exn (** Error, and possibly instance that triggered it *)
|
||||||
|
|
||||||
val check : ?rand:Random.State.t -> ?n:int ->
|
val check : ?rand:Random.State.t -> ?n:int ->
|
||||||
'a Arbitrary.t -> 'a Prop.t -> 'a result
|
'a Arbitrary.t -> 'a Prop.t -> 'a result
|
||||||
|
|
@ -227,12 +241,19 @@ type test
|
||||||
(** A single property test *)
|
(** A single property test *)
|
||||||
|
|
||||||
val mk_test : ?n:int -> ?pp:'a PP.t -> ?name:string ->
|
val mk_test : ?n:int -> ?pp:'a PP.t -> ?name:string ->
|
||||||
|
?size:('a -> int) -> ?limit:int ->
|
||||||
'a Arbitrary.t -> 'a Prop.t -> test
|
'a Arbitrary.t -> 'a Prop.t -> test
|
||||||
(** Construct a test. Optional parameters are the same as for {!run}.
|
(** Construct a test. Optional parameters are the same as for {!run}.
|
||||||
@param name is the name of the property that is checked
|
@param name is the name of the property that is checked
|
||||||
@param pp is a pretty printer for failing instances
|
@param pp is a pretty printer for failing instances
|
||||||
@out is the channel to print results onto
|
@out is the channel to print results onto
|
||||||
@rand is the random generator to use *)
|
@n is the number of tests (default 100)
|
||||||
|
@rand is the random generator to use
|
||||||
|
@size is a size function on values on which tests are performed. If
|
||||||
|
the test fails and a size function is given, the smallest
|
||||||
|
counter-examples with respect to [size] will be printed in priority.
|
||||||
|
@limit maximal number of counter-examples that will get printed.
|
||||||
|
Default is [10]. *)
|
||||||
|
|
||||||
val run : ?out:out_channel -> ?rand:Random.State.t -> test -> bool
|
val run : ?out:out_channel -> ?rand:Random.State.t -> test -> bool
|
||||||
(** Run a test and print results *)
|
(** Run a test and print results *)
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue