adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
authorbulwahn
Wed Jul 21 19:21:07 2010 +0200 (2010-07-21)
changeset 3792922e0797857e6
parent 37921 1e846be00ddf
child 37930 38e71ffc8fe8
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
src/HOL/ex/Quickcheck_Examples.thy
src/HOL/ex/Quickcheck_Lattice_Examples.thy
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/ex/Quickcheck_Examples.thy	Wed Jul 21 18:13:15 2010 +0200
     1.2 +++ b/src/HOL/ex/Quickcheck_Examples.thy	Wed Jul 21 19:21:07 2010 +0200
     1.3 @@ -19,27 +19,27 @@
     1.4  subsection {* Lists *}
     1.5  
     1.6  theorem "map g (map f xs) = map (g o f) xs"
     1.7 -  quickcheck
     1.8 +  quickcheck[expect = no_counterexample]
     1.9    oops
    1.10  
    1.11  theorem "map g (map f xs) = map (f o g) xs"
    1.12 -  quickcheck
    1.13 +  quickcheck[expect = counterexample]
    1.14    oops
    1.15  
    1.16  theorem "rev (xs @ ys) = rev ys @ rev xs"
    1.17 -  quickcheck
    1.18 +  quickcheck[expect = no_counterexample]
    1.19    oops
    1.20  
    1.21  theorem "rev (xs @ ys) = rev xs @ rev ys"
    1.22 -  quickcheck
    1.23 +  quickcheck[expect = counterexample]
    1.24    oops
    1.25  
    1.26  theorem "rev (rev xs) = xs"
    1.27 -  quickcheck
    1.28 +  quickcheck[expect = no_counterexample]
    1.29    oops
    1.30  
    1.31  theorem "rev xs = xs"
    1.32 -  quickcheck
    1.33 +  quickcheck[expect = counterexample]
    1.34    oops
    1.35  
    1.36  text {* An example involving functions inside other data structures *}
    1.37 @@ -49,11 +49,11 @@
    1.38    | "app (f # fs) x = app fs (f x)"
    1.39  
    1.40  lemma "app (fs @ gs) x = app gs (app fs x)"
    1.41 -  quickcheck
    1.42 +  quickcheck[expect = no_counterexample]
    1.43    by (induct fs arbitrary: x) simp_all
    1.44  
    1.45  lemma "app (fs @ gs) x = app fs (app gs x)"
    1.46 -  quickcheck
    1.47 +  quickcheck[expect = counterexample]
    1.48    oops
    1.49  
    1.50  primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
    1.51 @@ -67,16 +67,16 @@
    1.52  text {* A lemma, you'd think to be true from our experience with delAll *}
    1.53  lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
    1.54    -- {* Wrong. Precondition needed.*}
    1.55 -  quickcheck
    1.56 +  quickcheck[expect = counterexample]
    1.57    oops
    1.58  
    1.59  lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
    1.60 -  quickcheck
    1.61 +  quickcheck[expect = counterexample]
    1.62      -- {* Also wrong.*}
    1.63    oops
    1.64  
    1.65  lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
    1.66 -  quickcheck
    1.67 +  quickcheck[expect = no_counterexample]
    1.68    by (induct xs) auto
    1.69  
    1.70  primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.71 @@ -85,12 +85,12 @@
    1.72                              else (x#(replace a b xs)))"
    1.73  
    1.74  lemma "occurs a xs = occurs b (replace a b xs)"
    1.75 -  quickcheck
    1.76 +  quickcheck[expect = counterexample]
    1.77    -- {* Wrong. Precondition needed.*}
    1.78    oops
    1.79  
    1.80  lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
    1.81 -  quickcheck
    1.82 +  quickcheck[expect = no_counterexample]
    1.83    by (induct xs) simp_all
    1.84  
    1.85  
    1.86 @@ -113,12 +113,12 @@
    1.87    | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
    1.88  
    1.89  theorem "plant (rev (leaves xt)) = mirror xt"
    1.90 -  quickcheck
    1.91 +  quickcheck[expect = counterexample]
    1.92      --{* Wrong! *} 
    1.93    oops
    1.94  
    1.95  theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
    1.96 -  quickcheck
    1.97 +  quickcheck[expect = counterexample]
    1.98      --{* Wrong! *} 
    1.99    oops
   1.100  
   1.101 @@ -133,7 +133,7 @@
   1.102    | "root (Node f x y) = f"
   1.103  
   1.104  theorem "hd (inOrder xt) = root xt"
   1.105 -  quickcheck
   1.106 +  quickcheck[expect = counterexample]
   1.107      --{* Wrong! *} 
   1.108    oops
   1.109  
     2.1 --- a/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Wed Jul 21 18:13:15 2010 +0200
     2.2 +++ b/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Wed Jul 21 19:21:07 2010 +0200
     2.3 @@ -22,109 +22,109 @@
     2.4  
     2.5  lemma sup_inf_distrib2:
     2.6   "((y :: 'a :: distrib_lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
     2.7 -  quickcheck
     2.8 +  quickcheck[expect = no_counterexample]
     2.9  by(simp add: inf_sup_aci sup_inf_distrib1)
    2.10  
    2.11  lemma sup_inf_distrib2_1:
    2.12   "((y :: 'a :: lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
    2.13 -  quickcheck
    2.14 +  quickcheck[expect = counterexample]
    2.15    oops
    2.16  
    2.17  lemma sup_inf_distrib2_2:
    2.18   "((y :: 'a :: distrib_lattice) \<sqinter> z') \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
    2.19 -  quickcheck
    2.20 +  quickcheck[expect = counterexample]
    2.21    oops
    2.22  
    2.23  lemma inf_sup_distrib1_1:
    2.24   "(x :: 'a :: distrib_lattice) \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x' \<sqinter> z)"
    2.25 -  quickcheck
    2.26 +  quickcheck[expect = counterexample]
    2.27    oops
    2.28  
    2.29  lemma inf_sup_distrib2_1:
    2.30   "((y :: 'a :: distrib_lattice) \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (y \<sqinter> x)"
    2.31 -  quickcheck
    2.32 +  quickcheck[expect = counterexample]
    2.33    oops
    2.34  
    2.35  subsection {* Bounded lattices *}
    2.36  
    2.37  lemma inf_bot_left [simp]:
    2.38    "\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>"
    2.39 -  quickcheck
    2.40 +  quickcheck[expect = no_counterexample]
    2.41    by (rule inf_absorb1) simp
    2.42  
    2.43  lemma inf_bot_left_1:
    2.44    "\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = x"
    2.45 -  quickcheck
    2.46 +  quickcheck[expect = counterexample]
    2.47    oops
    2.48  
    2.49  lemma inf_bot_left_2:
    2.50    "y \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>"
    2.51 -  quickcheck
    2.52 +  quickcheck[expect = counterexample]
    2.53    oops
    2.54  
    2.55  lemma inf_bot_left_3:
    2.56    "x \<noteq> \<bottom> ==> y \<sqinter> (x :: 'a :: bounded_lattice_bot) \<noteq> \<bottom>"
    2.57 -  quickcheck
    2.58 +  quickcheck[expect = counterexample]
    2.59    oops
    2.60  
    2.61  lemma inf_bot_right [simp]:
    2.62    "(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> = \<bottom>"
    2.63 -  quickcheck
    2.64 +  quickcheck[expect = no_counterexample]
    2.65    by (rule inf_absorb2) simp
    2.66  
    2.67  lemma inf_bot_right_1:
    2.68    "x \<noteq> \<bottom> ==> (x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> = y"
    2.69 -  quickcheck
    2.70 +  quickcheck[expect = counterexample]
    2.71    oops
    2.72  
    2.73  lemma inf_bot_right_2:
    2.74    "(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> ~= \<bottom>"
    2.75 -  quickcheck
    2.76 +  quickcheck[expect = counterexample]
    2.77    oops
    2.78  
    2.79  lemma inf_bot_right [simp]:
    2.80    "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = \<bottom>"
    2.81 -  quickcheck
    2.82 +  quickcheck[expect = counterexample]
    2.83    oops
    2.84  
    2.85  lemma sup_bot_left [simp]:
    2.86    "\<bottom> \<squnion> (x :: 'a :: bounded_lattice_bot) = x"
    2.87 -  quickcheck
    2.88 +  quickcheck[expect = no_counterexample]
    2.89    by (rule sup_absorb2) simp
    2.90  
    2.91  lemma sup_bot_right [simp]:
    2.92    "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = x"
    2.93 -  quickcheck
    2.94 +  quickcheck[expect = no_counterexample]
    2.95    by (rule sup_absorb1) simp
    2.96  
    2.97  lemma sup_eq_bot_iff [simp]:
    2.98    "(x :: 'a :: bounded_lattice_bot) \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
    2.99 -  quickcheck
   2.100 +  quickcheck[expect = no_counterexample]
   2.101    by (simp add: eq_iff)
   2.102  
   2.103  lemma sup_top_left [simp]:
   2.104    "\<top> \<squnion> (x :: 'a :: bounded_lattice_top) = \<top>"
   2.105 -  quickcheck
   2.106 +  quickcheck[expect = no_counterexample]
   2.107    by (rule sup_absorb1) simp
   2.108  
   2.109  lemma sup_top_right [simp]:
   2.110    "(x :: 'a :: bounded_lattice_top) \<squnion> \<top> = \<top>"
   2.111 -  quickcheck
   2.112 +  quickcheck[expect = no_counterexample]
   2.113    by (rule sup_absorb2) simp
   2.114  
   2.115  lemma inf_top_left [simp]:
   2.116    "\<top> \<sqinter> x = (x :: 'a :: bounded_lattice_top)"
   2.117 -  quickcheck
   2.118 +  quickcheck[expect = no_counterexample]
   2.119    by (rule inf_absorb2) simp
   2.120  
   2.121  lemma inf_top_right [simp]:
   2.122    "x \<sqinter> \<top> = (x :: 'a :: bounded_lattice_top)"
   2.123 -  quickcheck
   2.124 +  quickcheck[expect = no_counterexample]
   2.125    by (rule inf_absorb1) simp
   2.126  
   2.127  lemma inf_eq_top_iff [simp]:
   2.128    "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
   2.129 -  quickcheck
   2.130 +  quickcheck[expect = no_counterexample]
   2.131    by (simp add: eq_iff)
   2.132  
   2.133  
     3.1 --- a/src/Tools/quickcheck.ML	Wed Jul 21 18:13:15 2010 +0200
     3.2 +++ b/src/Tools/quickcheck.ML	Wed Jul 21 19:21:07 2010 +0200
     3.3 @@ -13,8 +13,10 @@
     3.4    datatype report = Report of
     3.5      { iterations : int, raised_match_errors : int,
     3.6        satisfied_assms : int list, positive_concl_tests : int }
     3.7 +  datatype expectation = No_Expectation | No_Counterexample | Counterexample;
     3.8    datatype test_params = Test_Params of
     3.9 -  { size: int, iterations: int, default_type: typ list, no_assms: bool, report: bool, quiet : bool};
    3.10 +  { size: int, iterations: int, default_type: typ list, no_assms: bool,
    3.11 +    expect : expectation, report: bool, quiet : bool};
    3.12    val test_params_of: theory -> test_params 
    3.13    val add_generator:
    3.14      string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))
    3.15 @@ -65,32 +67,41 @@
    3.16           (if null satisfied_assms then replicate (length assms) 0 else satisfied_assms),
    3.17        positive_concl_tests = if concl then positive_concl_tests + 1 else positive_concl_tests}
    3.18  
    3.19 +(* expectation *)
    3.20 +
    3.21 +datatype expectation = No_Expectation | No_Counterexample | Counterexample; 
    3.22 +
    3.23 +fun merge_expectation (expect1, expect2) =
    3.24 +  if expect1 = expect2 then expect1 else No_Expectation
    3.25 +
    3.26  (* quickcheck configuration -- default parameters, test generators *)
    3.27  
    3.28  datatype test_params = Test_Params of
    3.29 -  { size: int, iterations: int, default_type: typ list, no_assms: bool, report: bool, quiet : bool};
    3.30 +  { size: int, iterations: int, default_type: typ list, no_assms: bool,
    3.31 +  expect : expectation, report: bool, quiet : bool};
    3.32  
    3.33 -fun dest_test_params (Test_Params { size, iterations, default_type, no_assms, report, quiet }) =
    3.34 -  ((size, iterations), ((default_type, no_assms), (report, quiet)));
    3.35 -fun make_test_params ((size, iterations), ((default_type, no_assms), (report, quiet))) =
    3.36 +fun dest_test_params (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) =
    3.37 +  ((size, iterations), ((default_type, no_assms), ((expect, report), quiet)));
    3.38 +fun make_test_params ((size, iterations), ((default_type, no_assms), ((expect, report), quiet))) =
    3.39    Test_Params { size = size, iterations = iterations, default_type = default_type,
    3.40 -                no_assms = no_assms, report = report, quiet = quiet };
    3.41 -fun map_test_params f (Test_Params { size, iterations, default_type, no_assms, report, quiet }) =
    3.42 -  make_test_params (f ((size, iterations), ((default_type, no_assms), (report, quiet))));
    3.43 +                no_assms = no_assms, expect = expect, report = report, quiet = quiet };
    3.44 +fun map_test_params f (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) =
    3.45 +  make_test_params (f ((size, iterations), ((default_type, no_assms), ((expect, report), quiet))));
    3.46  fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
    3.47 -                                     no_assms = no_assms1, report = report1, quiet = quiet1 },
    3.48 +                                     no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1 },
    3.49    Test_Params { size = size2, iterations = iterations2, default_type = default_type2,
    3.50 -                no_assms = no_assms2, report = report2, quiet = quiet2 }) =
    3.51 +                no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2 }) =
    3.52    make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
    3.53      ((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2),
    3.54 -    (report1 orelse report2, quiet1 orelse quiet2)));
    3.55 +    ((merge_expectation (expect1, expect2), report1 orelse report2), quiet1 orelse quiet2)));
    3.56  
    3.57  structure Data = Theory_Data
    3.58  (
    3.59    type T = (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list
    3.60      * test_params;
    3.61    val empty = ([], Test_Params
    3.62 -    { size = 10, iterations = 100, default_type = [], no_assms = false, report = false, quiet = false});
    3.63 +    { size = 10, iterations = 100, default_type = [], no_assms = false,
    3.64 +      expect = No_Expectation, report = false, quiet = false});
    3.65    val extend = I;
    3.66    fun merge ((generators1, params1), (generators2, params2)) : T =
    3.67      (AList.merge (op =) (K true) (generators1, generators2),
    3.68 @@ -271,7 +282,7 @@
    3.69      let
    3.70        val ctxt = Proof.context_of state;
    3.71        val assms = map term_of (Assumption.all_assms_of ctxt);
    3.72 -      val Test_Params { size, iterations, default_type, no_assms, report, quiet } =
    3.73 +      val Test_Params {size, iterations, default_type, no_assms, ...} =
    3.74          (snd o Data.get o Proof.theory_of) state;
    3.75        val res =
    3.76          try (test_goal true false NONE size iterations default_type no_assms [] 1 assms) state;
    3.77 @@ -297,6 +308,11 @@
    3.78    | read_bool "true" = true
    3.79    | read_bool s = error ("Not a Boolean value: " ^ s)
    3.80  
    3.81 +fun read_expectation "no_expectation" = No_Expectation
    3.82 +  | read_expectation "no_counterexample" = No_Counterexample 
    3.83 +  | read_expectation "counterexample" = Counterexample
    3.84 +  | read_expectation s = error ("Not an expectation value: " ^ s)  
    3.85 +
    3.86  fun parse_test_param ctxt ("size", [arg]) =
    3.87        (apfst o apfst o K) (read_nat arg)
    3.88    | parse_test_param ctxt ("iterations", [arg]) =
    3.89 @@ -305,10 +321,12 @@
    3.90        (apsnd o apfst o apfst o K) (map (ProofContext.read_typ ctxt) arg)
    3.91    | parse_test_param ctxt ("no_assms", [arg]) =
    3.92        (apsnd o apfst o apsnd o K) (read_bool arg)
    3.93 +  | parse_test_param ctxt ("expect", [arg]) =
    3.94 +      (apsnd o apsnd o apfst o apfst o K) (read_expectation arg)
    3.95    | parse_test_param ctxt ("report", [arg]) =
    3.96 -      (apsnd o apsnd o apfst o K) (read_bool arg)
    3.97 +      (apsnd o apsnd o apfst o apsnd o K) (read_bool arg)
    3.98    | parse_test_param ctxt ("quiet", [arg]) =
    3.99 -      (apsnd o apsnd o apsnd o K) (read_bool arg)
   3.100 +      (apsnd o apsnd o apsnd o K) (read_bool arg)       
   3.101    | parse_test_param ctxt (name, _) =
   3.102        error ("Unknown test parameter: " ^ name);
   3.103  
   3.104 @@ -336,10 +354,14 @@
   3.105      val assms = map term_of (Assumption.all_assms_of ctxt);
   3.106      val default_params = (dest_test_params o snd o Data.get) thy;
   3.107      val f = fold (parse_test_param_inst ctxt) args;
   3.108 -    val (((size, iterations), ((default_type, no_assms), (report, quiet))), (generator_name, insts)) =
   3.109 +    val (((size, iterations), ((default_type, no_assms), ((expect, report), quiet))), (generator_name, insts)) =
   3.110        f (default_params, (NONE, []));
   3.111    in
   3.112      test_goal quiet report generator_name size iterations default_type no_assms insts i assms state
   3.113 +    |> tap (fn (SOME x, _) => if expect = No_Counterexample then
   3.114 +                 error ("quickcheck expect to find no counterexample but found one") else ()
   3.115 +             | (NONE, _) => if expect = Counterexample then
   3.116 +                 error ("quickcheck expected to find a counterexample but did not find one") else ())
   3.117    end;
   3.118  
   3.119  fun quickcheck args i state = fst (gen_quickcheck args i state);