39186
|
1 |
theory IMP_3
|
|
2 |
imports "Predicate_Compile_Quickcheck"
|
|
3 |
begin
|
|
4 |
|
|
5 |
subsection {* IMP *}
|
|
6 |
|
|
7 |
text {*
|
|
8 |
In this example, the state is one integer variable and the commands are Skip, Ass, Seq, IF, and While.
|
|
9 |
*}
|
|
10 |
|
|
11 |
types
|
|
12 |
var = unit
|
|
13 |
state = int
|
|
14 |
|
|
15 |
datatype com =
|
|
16 |
Skip |
|
|
17 |
Ass var "int" |
|
|
18 |
Seq com com |
|
|
19 |
IF "state list" com com |
|
|
20 |
While "state list" com
|
|
21 |
|
|
22 |
inductive exec :: "com => state => state => bool" where
|
|
23 |
"exec Skip s s" |
|
|
24 |
"exec (Ass x e) s e" |
|
|
25 |
"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
|
|
26 |
"s \<in> set b ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
|
|
27 |
"s \<notin> set b ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
|
|
28 |
"s \<notin> set b ==> exec (While b c) s s" |
|
|
29 |
"s1 \<in> set b ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
|
|
30 |
|
|
31 |
lemma
|
|
32 |
"exec c s s' ==> exec (Seq c c) s s'"
|
40924
|
33 |
quickcheck[tester = predicate_compile_ff_nofs, size=2, iterations=10, quiet = false, expect = counterexample]
|
39186
|
34 |
oops
|
|
35 |
|
|
36 |
|
|
37 |
end |