equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Examples for narrowing-based testing *} |
6 header {* Examples for narrowing-based testing *} |
7 |
7 |
8 theory Quickcheck_Narrowing_Examples |
8 theory Quickcheck_Narrowing_Examples |
9 imports "~~/src/HOL/Library/LSC" |
9 imports "~~/src/HOL/Library/Quickcheck_Narrowing" |
10 begin |
10 begin |
11 |
11 |
12 subsection {* Simple list examples *} |
12 subsection {* Simple list examples *} |
13 |
13 |
14 lemma "rev xs = xs" |
14 lemma "rev xs = xs" |
15 quickcheck[tester = lazy_exhaustive, finite_types = false, default_type = nat, expect = counterexample] |
15 quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample] |
16 oops |
16 oops |
17 |
17 |
18 text {* Example fails due to some strange thing... *} |
18 text {* Example fails due to some strange thing... *} |
19 (* |
19 (* |
20 lemma "rev xs = xs" |
20 lemma "rev xs = xs" |
132 |
132 |
133 subsubsection {* Invalid Lemma due to typo in lbal *} |
133 subsubsection {* Invalid Lemma due to typo in lbal *} |
134 |
134 |
135 lemma is_ord_l_bal: |
135 lemma is_ord_l_bal: |
136 "\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))" |
136 "\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))" |
137 quickcheck[tester = lazy_exhaustive, finite_types = false, default_type = nat, size = 1, timeout = 100, expect = counterexample] |
137 quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 1, timeout = 100, expect = counterexample] |
138 oops |
138 oops |
139 |
139 |
140 |
140 |
141 end |
141 end |