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