diff --git a/qCheck.ml b/qCheck.ml index a776a771..b971ad7f 100644 --- a/qCheck.ml +++ b/qCheck.ml @@ -43,6 +43,12 @@ module Arbitrary = struct 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 float f st = Random.State.float st f @@ -90,24 +96,26 @@ module Arbitrary = struct Array.init n (fun _ -> ar 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 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 = - assert (l <> []); - let a = Array.of_list l in - fun st -> - let i = Random.State.int st (Array.length a) in - a.(i) st + let choose l = match l with + | [] -> failwith "cannot choose from empty list" + | [x] -> x + | _ -> + let a = Array.of_list l in + fun st -> + let i = Random.State.int st (Array.length a) in + a.(i) st - let _fix ~max ~depth recursive 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 fix ?(max=15) ~base f = let rec ar = lazy (fun depth st -> if depth >= max || Random.State.int st max < depth @@ -122,6 +130,10 @@ module Arbitrary = struct let max = depth st in 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 lift2 f a b st = f (a st) (b st) @@ -169,22 +181,22 @@ module PP = struct let list pp l = let b = Buffer.create 25 in - Buffer.add_char b '('; + Buffer.add_char b '['; List.iteri (fun i x -> if i > 0 then Buffer.add_string b ", "; Buffer.add_string b (pp x)) l; - Buffer.add_char b ')'; + Buffer.add_char b ']'; Buffer.contents b let array pp a = let b = Buffer.create 25 in - Buffer.add_char b '['; + Buffer.add_string b "[|"; Array.iteri (fun i x -> if i > 0 then Buffer.add_string b ", "; Buffer.add_string b (pp x)) a; - Buffer.add_char b ']'; + Buffer.add_string b "|]"; Buffer.contents b end @@ -216,7 +228,7 @@ end type 'a result = | Ok of int * int (* total number / precond failed *) | Failed of 'a list - | Error of exn + | Error of 'a option * exn (* random seed, for repeatability of tests *) 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 precond_failed = ref 0 in let failures = ref [] in + let inst = ref None in try for i = 0 to n - 1 do let x = gen rand in + inst := Some x; try if not (prop x) then failures := x :: !failures @@ -237,7 +251,7 @@ let check ?(rand=Random.State.make __seed) ?(n=100) gen prop = | [] -> Ok (n, !precond_failed) | _ -> Failed (!failures) with e -> - Error e + Error (!inst, e) (** {2 Main} *) @@ -247,13 +261,23 @@ type 'a test_cell = { prop : 'a Prop.t; gen : 'a Arbitrary.t; name : string; + limit : int; + size : ('a -> int) option; } type test = | Test : 'a test_cell -> test (** GADT needed for the existential type *) -let mk_test ?(n=100) ?pp ?(name="") gen prop = - Test { prop; gen; name; n; pp; } +let mk_test ?(n=100) ?pp ?(name="") ?size ?(limit=10) gen prop = + 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) = 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 | Failed l -> 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 -> - 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 (fun x -> Printf.fprintf out " %s\n" (pp x)) - l + to_print end; false - | Error e -> - Printf.fprintf out " [×] error: %s\n" (Printexc.to_string e); + | Error (inst, 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 type suite = test list @@ -281,11 +324,12 @@ let flatten = List.flatten let run_tests ?(out=stdout) ?(rand=Random.State.make __seed) l = let start = Unix.gettimeofday () in + let n = List.length l in let failed = ref 0 in Printf.fprintf out "check %d properties...\n" (List.length 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); if !failed = 0 - then Printf.fprintf out "[✔] Success!\n" - else Printf.fprintf out "[×] Failure (%d tests failed).\n" !failed; + then Printf.fprintf out "[✔] Success! (passed %d tests)\n" n + else Printf.fprintf out "[×] Failure. (%d tests failed over %d)\n" !failed n; !failed = 0 diff --git a/qCheck.mli b/qCheck.mli index c294623d..6b59f0a0 100644 --- a/qCheck.mli +++ b/qCheck.mli @@ -49,14 +49,6 @@ number of instances to generate and test... 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: {[ @@ -64,8 +56,20 @@ let test = QCheck.mk_test ~n:1000 QCheck.Arbitrary.(list alpha) (fun l -> List.rev (List.rev l) = l);; 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;; @@ -73,7 +77,7 @@ QCheck.run test;; ~base:(map small_int (fun i -> Int i)) (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 (* Integer range start .. stop-1 *) + val (--) : int -> int -> int t + (** Infix synonym for {!int_range} *) + val small_int : int t (** 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 (** Arbitrary boolean *) @@ -117,7 +128,7 @@ module Arbitrary : sig (** Transform an arbitrary into another *) 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 (** 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 (** 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 (** Recursive values of at most given random depth *) @@ -161,6 +172,9 @@ module Arbitrary : sig val (>>=) : 'a t -> ('a -> 'b t) -> 'b t (** 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 (** Generate [n] random values of the given type *) end @@ -213,8 +227,8 @@ end type 'a result = | Ok of int * int (** total number of tests / number of failed preconditions *) - | Failed of 'a list - | Error of exn + | Failed of 'a list (** Failed instances *) + | Error of 'a option * exn (** Error, and possibly instance that triggered it *) val check : ?rand:Random.State.t -> ?n:int -> 'a Arbitrary.t -> 'a Prop.t -> 'a result @@ -227,12 +241,19 @@ type test (** A single property test *) val mk_test : ?n:int -> ?pp:'a PP.t -> ?name:string -> + ?size:('a -> int) -> ?limit:int -> 'a Arbitrary.t -> 'a Prop.t -> test (** Construct a test. Optional parameters are the same as for {!run}. @param name is the name of the property that is checked @param pp is a pretty printer for failing instances @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 (** Run a test and print results *)