1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Crunch_Test_Trace 8imports 9 Lib.Crunch_Instances_Trace 10 Crunch_Test_Qualified_Trace 11 Lib.Defs 12begin 13 14text \<open>Test cases for crunch\<close> 15 16definition 17 "crunch_foo1 (x :: nat) \<equiv> do 18 modify ((+) x); 19 modify ((+) x) 20 od" 21 22definition 23 "crunch_foo2 \<equiv> do 24 crunch_foo1 12; 25 crunch_foo1 13 26 od" 27 28crunch_ignore (add: crunch_foo1) 29 30crunch gt: crunch_foo2 "\<lambda>x. x > y" 31 (ignore: modify bind ignore_del: crunch_foo1) 32 33crunch_ignore (del: crunch_foo1) 34 35definition 36 "crunch_always_true (x :: nat) \<equiv> \<lambda>y :: nat. True" 37 38lemma crunch_foo1_at_2: 39 "True \<Longrightarrow> \<lbrace>crunch_always_true 3 and crunch_always_true 2\<rbrace> 40 crunch_foo1 x \<lbrace>\<lambda>rv. crunch_always_true 2 and K True\<rbrace>" 41 by (simp add: crunch_always_true_def, wp) 42 43lemma crunch_foo1_at_3[wp]: 44 "\<lbrace>crunch_always_true 3\<rbrace> crunch_foo1 x \<lbrace>\<lambda>rv. crunch_always_true 3\<rbrace>" 45 by (simp add: crunch_always_true_def, wp) 46 47lemma crunch_foo1_no_fail: 48 "True \<Longrightarrow> no_fail (crunch_always_true 2 and crunch_always_true 3) (crunch_foo1 x)" 49 apply (simp add:crunch_always_true_def crunch_foo1_def) 50 apply (rule no_fail_pre) 51 apply (wp, simp) 52 done 53 54crunch (no_fail) no_fail: crunch_foo2 55 (ignore: modify bind wp: crunch_foo1_at_2[simplified]) 56 57crunch (valid) at_2: crunch_foo2 "crunch_always_true 2" 58 (ignore: modify bind wp: crunch_foo1_at_2[simplified]) 59 60fun crunch_foo3 :: "nat => nat => 'a => (nat,unit) tmonad" where 61 "crunch_foo3 0 x _ = crunch_foo1 x" 62| "crunch_foo3 (Suc n) x y = crunch_foo3 n x y" 63 64crunch gt2: crunch_foo3 "\<lambda>x. x > y" 65 (ignore: modify bind) 66 67class foo_class = 68 fixes stuff :: 'a 69begin 70 71fun crunch_foo4 :: "nat => nat => 'a => (nat,unit) tmonad" where 72 "crunch_foo4 0 x _ = crunch_foo1 x" 73| "crunch_foo4 (Suc n) x y = crunch_foo4 n x y" 74 75definition 76 "crunch_foo5 x (y::'a) \<equiv> crunch_foo1 x" 77 78end 79 80lemma crunch_foo4_alt: 81 "crunch_foo4 n x y \<equiv> crunch_foo1 x" 82 apply (induct n) 83 apply simp+ 84 done 85 86crunch gt3: crunch_foo4 "\<lambda>x. x > y" 87 (ignore: modify bind) 88 89crunch (no_fail) no_fail2: crunch_foo4 90 (rule: crunch_foo4_alt ignore: modify bind) 91 92crunch gt3': crunch_foo4 "\<lambda>x. x > y" 93 (rule: crunch_foo4_alt ignore: modify bind) 94 95crunch gt4: crunch_foo5 "\<lambda>x. x > y" 96 (ignore: modify bind) 97 98(* Test cases for crunch in locales *) 99 100definition 101 "crunch_foo6 \<equiv> return () >>= (\<lambda>_. return ())" 102 103locale test_locale = 104fixes fixed_return_unit :: "(unit, unit) tmonad" 105 106begin 107 108definition 109 "crunch_foo7 \<equiv> return () >>= (\<lambda>_. return ())" 110 111(* crunch works on a global constant within a locale *) 112crunch test[wp]: crunch_foo6 P 113(ignore: bind) 114 115(* crunch works on a locale constant *) 116crunch test[wp]: crunch_foo7 P 117(ignore: bind) 118 119definition 120 "crunch_foo8 \<equiv> fixed_return_unit >>= (\<lambda>_. fixed_return_unit)" 121 122definition 123 "crunch_foo9 (x :: nat) \<equiv> do 124 modify ((+) x); 125 modify ((+) x) 126 od" 127 128crunch test: crunch_foo9 "\<lambda>x. x > y" (ignore: bind) 129 130definition 131 "crunch_foo10 (x :: nat) \<equiv> do 132 modify ((+) x); 133 modify ((+) x) 134 od" 135 136(*crunch_def attribute overrides definition lookup *) 137 138lemma crunch_foo10_def2[crunch_def]: 139 "crunch_foo10 = crunch_foo9" 140 unfolding crunch_foo10_def[abs_def] crunch_foo9_def[abs_def] 141 by simp 142 143crunch test[wp]: crunch_foo10 "\<lambda>x. x > y" 144 145(* crunch_ignore works within a locale *) 146crunch_ignore (add: bind) 147 148crunch test': crunch_foo9 "\<lambda>x. x > y" 149 150end 151 152interpretation test_locale "return ()" . 153 154(* interpretation promotes the wp attribute from the locale *) 155lemma "\<lbrace>Q\<rbrace> crunch_foo7 \<lbrace>\<lambda>_. Q\<rbrace>" by wp 156 157(* crunch still works on an interpreted locale constant *) 158crunch test2: crunch_foo7 P 159 (wp_del: crunch_foo7_test) 160 161locale test_sublocale 162 163sublocale test_sublocale < test_locale "return ()" . 164 165context test_sublocale begin 166 167(* crunch works on a locale constant with a fixed locale parameter *) 168crunch test[wp]: crunch_foo8 P 169 170end 171 172(* check that qualified names are handled properly. *) 173 174consts foo_const :: "(unit, unit) tmonad" 175defs foo_const_def: "foo_const \<equiv> Crunch_Test_Qualified_Trace.foo_const" 176 177crunch test: foo_const P 178 179(* check that the grid-style crunch is working *) 180 181crunches crunch_foo3, crunch_foo4, crunch_foo5 182 for silly: "\<lambda>s. True \<noteq> False" and (no_fail)nf 183 (ignore: modify bind rule: crunch_foo4_alt wp_del: hoare_vcg_prop) 184 185end 186