updated QCheck, adding test/suite types, more Arbitrary, PP and Prop functions

This commit is contained in:
Simon Cruanes 2013-10-04 14:45:48 +02:00
parent b3c76eb897
commit 4c46f9a697
2 changed files with 115 additions and 21 deletions

View file

@ -29,6 +29,8 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
module Arbitrary = struct module Arbitrary = struct
type 'a t = Random.State.t -> 'a type 'a t = Random.State.t -> 'a
let return x st = x
let int n st = Random.State.int st n let int n st = Random.State.int st n
let int_range ~start ~stop st = let int_range ~start ~stop st =
@ -117,6 +119,27 @@ module Arbitrary = struct
let fix_depth ~depth ~base f st = let fix_depth ~depth ~base f st =
let max = depth st in let max = depth st in
fix ~max ~base f st fix ~max ~base f st
let lift f a st = f (a st)
let lift2 f a b st = f (a st) (b st)
let lift3 f a b c st = f (a st) (b st) (c st)
let lift4 f a b c d st = f (a st) (b st) (c st) (d st)
let pair a b = lift2 (fun x y -> x,y) a b
let triple a b c = lift3 (fun x y z -> x,y,z) a b c
let quad a b c d = lift4 (fun x y z w -> x,y,z,w) a b c d
let generate ?(n=100) ?(rand=Random.State.make_self_init()) gen =
let l = ref [] in
for i = 0 to n-1 do
l := (gen rand) :: !l
done;
!l
end end
(** {2 Pretty printing} *) (** {2 Pretty printing} *)
@ -133,6 +156,11 @@ module PP = struct
s.[0] <- c; s.[0] <- c;
s s
let pair a b (x,y) = Printf.sprintf "(%s, %s)" (a x) (b y)
let triple a b c (x,y,z) = Printf.sprintf "(%s, %s, %s)" (a x) (b y) (c z)
let quad a b c d (x,y,z,w) =
Printf.sprintf "(%s, %s, %s, %s)" (a x) (b y) (c z) (d w)
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 '(';
@ -161,9 +189,16 @@ module Prop = struct
exception PrecondFail exception PrecondFail
let assume p =
if not p then raise PrecondFail
let assume_lazy (lazy p) =
if not p then raise PrecondFail
let (==>) a b = let (==>) a b =
fun x -> fun x ->
if not (a x) then raise PrecondFail else b x assume (a x);
b x
let (&&&) a b x = a x && b x let (&&&) a b x = a x && b x
@ -197,31 +232,49 @@ let check ?(rand=Random.State.make_self_init ()) ?(n=100) gen prop =
(** {2 Main} *) (** {2 Main} *)
let run ?pp ?n ?(rand=Random.State.make_self_init()) ?(name="<no name>") gen prop = type 'a test_cell = {
Printf.printf "testing property %s...\n" name; n : int;
match check ~rand ?n gen prop with pp : 'a PP.t option;
prop : 'a Prop.t;
gen : 'a Arbitrary.t;
name : string;
}
type test =
| Test : 'a test_cell -> test
(** GADT needed for the existential type *)
let mk_test ?(n=100) ?pp ?(name="<anon prop>") gen prop =
Test { prop; gen; name; n; pp; }
let run ?(out=stdout) ?(rand=Random.State.make_self_init()) (Test test) =
Printf.fprintf out "testing property %s...\n" test.name;
match check ~rand ~n:test.n test.gen test.prop with
| Ok (n, prefail) -> | Ok (n, prefail) ->
Printf.printf "passed %d tests (%d preconditions failed)\n" n prefail; Printf.fprintf out "passed %d tests (%d preconditions failed)\n" n prefail;
true true
| Failed l -> | Failed l ->
begin match pp with begin match test.pp with
| None -> Printf.printf "%d failures\n" (List.length l) | None -> Printf.fprintf out "%d failures\n" (List.length l)
| Some pp -> | Some pp ->
Printf.printf "%d failures:\n" (List.length l); Printf.fprintf out "%d failures:\n" (List.length l);
List.iter List.iter
(fun x -> Printf.printf " %s\n" (pp x)) (fun x -> Printf.fprintf out " %s\n" (pp x))
l l
end; end;
false false
| Error e -> | Error e ->
Printf.printf "error: %s\n" (Printexc.to_string e); Printf.fprintf out "error: %s\n" (Printexc.to_string e);
false false
let run_tests l = type suite = test list
let rand = Random.State.make_self_init () in
let flatten = List.flatten
let run_tests ?(out=stdout) ?(rand=Random.State.make_self_init()) l =
let res = ref true in let res = ref true in
List.iter (fun test -> if not (test ~rand) then res := false) l; Printf.fprintf out "check %d properties...\n" (List.length l);
List.iter (fun test -> if not (run ~out ~rand test) then res := false) l;
if !res if !res
then Printf.printf "Success!\n" then Printf.fprintf out "Success!\n"
else Printf.printf "Failure.\n"; else Printf.fprintf out "Failure.\n";
!res !res

View file

@ -79,6 +79,9 @@ module Arbitrary : sig
type 'a t = Random.State.t -> 'a type 'a t = Random.State.t -> 'a
(** A generator of arbitrary values of type 'a *) (** A generator of arbitrary values of type 'a *)
val return : 'a -> 'a t
(** Return always the same value (e.g. [4]) *)
val int : int -> int t val int : int -> int t
(** Any integer between 0 (inclusive) and the given higher bound (exclusive) *) (** Any integer between 0 (inclusive) and the given higher bound (exclusive) *)
@ -115,6 +118,12 @@ module Arbitrary : sig
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 *)
val pair : 'a t -> 'b t -> ('a * 'b) t
val triple : 'a t -> 'b t -> 'c t -> ('a * 'b * 'c) t
val quad : 'a t -> 'b t -> 'c t -> 'd t -> ('a * 'b * 'c * 'd) t
val list_repeat : int -> 'a t -> 'a list t val list_repeat : int -> 'a t -> 'a list t
(** Lists of given length exactly *) (** Lists of given length exactly *)
@ -139,6 +148,14 @@ module Arbitrary : sig
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 *)
val lift : ('a -> 'b) -> 'a t -> 'b t
val lift2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
val lift3 : ('a -> 'b -> 'c -> 'd) -> 'a t -> 'b t -> 'c t -> 'd t
val lift4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a t -> 'b t -> 'c t -> 'd t -> 'e t
val generate : ?n:int -> ?rand:Random.State.t -> 'a t -> 'a list
(** Generate [n] random values of the given type *)
end end
(** {2 Pretty printing} *) (** {2 Pretty printing} *)
@ -152,6 +169,10 @@ module PP : sig
val char : char t val char : char t
val string : string t val string : string t
val pair : 'a t -> 'b t -> ('a*'b) t
val triple : 'a t -> 'b t -> 'c t -> ('a*'b*'c) t
val quad : 'a t -> 'b t -> 'c t -> 'd t -> ('a*'b*'c*'d) t
val list : 'a t -> 'a list t val list : 'a t -> 'a list t
val array : 'a t -> 'a array t val array : 'a t -> 'a array t
end end
@ -164,6 +185,12 @@ module Prop : sig
val (==>) : ('a -> bool) -> 'a t -> 'a t val (==>) : ('a -> bool) -> 'a t -> 'a t
(** Precondition for a test *) (** Precondition for a test *)
val assume : bool -> unit
(** Assume the given precondition holds *)
val assume_lazy : bool lazy_t -> unit
(** Assume the given (lazy) precondition holds *)
val (&&&) : 'a t -> 'a t -> 'a t val (&&&) : 'a t -> 'a t -> 'a t
(** Logical 'and' on tests *) (** Logical 'and' on tests *)
@ -186,10 +213,24 @@ val check : ?rand:Random.State.t -> ?n:int ->
(** {2 Main} *) (** {2 Main} *)
val run : ?pp:('a -> string) -> ?n:int -> type test
?rand:Random.State.t -> ?name:string -> (** A single property test *)
'a Arbitrary.t -> 'a Prop.t -> bool
(** Run and print result *)
val run_tests : (rand:Random.State.t -> bool) list -> bool val mk_test : ?n:int -> ?pp:'a PP.t -> ?name:string ->
(** Run a list of tests, and print their results *) '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 *)
val run : ?out:out_channel -> ?rand:Random.State.t -> test -> bool
(** Run a test and print results *)
type suite = test list
(** A test suite is a list of tests *)
val flatten : suite list -> suite
val run_tests : ?out:out_channel -> ?rand:Random.State.t -> suite -> bool
(** Run a suite of tests, and print its results *)