author | kleing |
Sat, 13 Aug 2011 11:57:13 +0200 | |
changeset 44177 | b4b5cbca2519 |
parent 43738 | e40d2eddf2c0 |
child 45200 | 1f1897ac7877 |
permissions | -rw-r--r-- |
43158 | 1 |
theory C_like imports Main begin |
2 |
||
3 |
subsection "A C-like Language" |
|
4 |
||
5 |
type_synonym state = "nat \<Rightarrow> nat" |
|
6 |
||
7 |
datatype aexp = N nat | Deref aexp ("!") | Plus aexp aexp |
|
8 |
||
9 |
fun aval :: "aexp \<Rightarrow> state \<Rightarrow> nat" where |
|
10 |
"aval (N n) s = n" | |
|
11 |
"aval (!a) s = s(aval a s)" | |
|
12 |
"aval (Plus a\<^isub>1 a\<^isub>2) s = aval a\<^isub>1 s + aval a\<^isub>2 s" |
|
13 |
||
14 |
datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp |
|
15 |
||
16 |
primrec bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where |
|
17 |
"bval (B bv) _ = bv" | |
|
18 |
"bval (Not b) s = (\<not> bval b s)" | |
|
19 |
"bval (And b\<^isub>1 b\<^isub>2) s = (if bval b\<^isub>1 s then bval b\<^isub>2 s else False)" | |
|
20 |
"bval (Less a\<^isub>1 a\<^isub>2) s = (aval a\<^isub>1 s < aval a\<^isub>2 s)" |
|
21 |
||
22 |
||
23 |
datatype |
|
24 |
com = SKIP |
|
25 |
| Assign aexp aexp ("_ ::= _" [61, 61] 61) |
|
26 |
| New aexp aexp |
|
27 |
| Semi com com ("_;/ _" [60, 61] 60) |
|
28 |
| If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) |
|
29 |
| While bexp com ("(WHILE _/ DO _)" [0, 61] 61) |
|
30 |
||
31 |
inductive |
|
32 |
big_step :: "com \<times> state \<times> nat \<Rightarrow> state \<times> nat \<Rightarrow> bool" (infix "\<Rightarrow>" 55) |
|
33 |
where |
|
34 |
Skip: "(SKIP,sn) \<Rightarrow> sn" | |
|
35 |
Assign: "(lhs ::= a,s,n) \<Rightarrow> (s(aval lhs s := aval a s),n)" | |
|
36 |
New: "(New lhs a,s,n) \<Rightarrow> (s(aval lhs s := n), n+aval a s)" | |
|
37 |
Semi: "\<lbrakk> (c\<^isub>1,sn\<^isub>1) \<Rightarrow> sn\<^isub>2; (c\<^isub>2,sn\<^isub>2) \<Rightarrow> sn\<^isub>3 \<rbrakk> \<Longrightarrow> |
|
38 |
(c\<^isub>1;c\<^isub>2, sn\<^isub>1) \<Rightarrow> sn\<^isub>3" | |
|
39 |
||
40 |
IfTrue: "\<lbrakk> bval b s; (c\<^isub>1,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow> |
|
41 |
(IF b THEN c\<^isub>1 ELSE c\<^isub>2, s,n) \<Rightarrow> tn" | |
|
42 |
IfFalse: "\<lbrakk> \<not>bval b s; (c\<^isub>2,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow> |
|
43 |
(IF b THEN c\<^isub>1 ELSE c\<^isub>2, s,n) \<Rightarrow> tn" | |
|
44 |
||
45 |
WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s,n) \<Rightarrow> (s,n)" | |
|
46 |
WhileTrue: |
|
47 |
"\<lbrakk> bval b s\<^isub>1; (c,s\<^isub>1,n) \<Rightarrow> sn\<^isub>2; (WHILE b DO c, sn\<^isub>2) \<Rightarrow> sn\<^isub>3 \<rbrakk> \<Longrightarrow> |
|
48 |
(WHILE b DO c, s\<^isub>1,n) \<Rightarrow> sn\<^isub>3" |
|
49 |
||
50 |
code_pred big_step . |
|
51 |
||
43738
e40d2eddf2c0
adding a very liberal timeout for values after a test case failed due to the restricted timeout
bulwahn
parents:
43158
diff
changeset
|
52 |
declare [[values_timeout = 3600]] |
43158 | 53 |
|
54 |
text{* Examples: *} |
|
55 |
||
56 |
definition |
|
57 |
"array_sum = |
|
58 |
WHILE Less (!(N 0)) (Plus (!(N 1)) (N 1)) |
|
59 |
DO ( N 2 ::= Plus (!(N 2)) (!(!(N 0))); |
|
60 |
N 0 ::= Plus (!(N 0)) (N 1) )" |
|
61 |
||
62 |
text {* To show the first n variables in a @{typ "nat \<Rightarrow> nat"} state: *} |
|
63 |
definition |
|
64 |
"list t n = map t [0 ..< n]" |
|
65 |
||
66 |
values "{list t n |t n. (array_sum, nth[3,4,0,3,7],5) \<Rightarrow> (t,n)}" |
|
67 |
||
68 |
definition |
|
69 |
"linked_list_sum = |
|
70 |
WHILE Less (N 0) (!(N 0)) |
|
71 |
DO ( N 1 ::= Plus(!(N 1)) (!(!(N 0))); |
|
72 |
N 0 ::= !(Plus(!(N 0))(N 1)) )" |
|
73 |
||
74 |
values "{list t n |t n. (linked_list_sum, nth[4,0,3,0,7,2],6) \<Rightarrow> (t,n)}" |
|
75 |
||
76 |
definition |
|
77 |
"array_init = |
|
78 |
New (N 0) (!(N 1)); N 2 ::= !(N 0); |
|
79 |
WHILE Less (!(N 2)) (Plus (!(N 0)) (!(N 1))) |
|
80 |
DO ( !(N 2) ::= !(N 2); |
|
81 |
N 2 ::= Plus (!(N 2)) (N 1) )" |
|
82 |
||
83 |
values "{list t n |t n. (array_init, nth[5,2,7],3) \<Rightarrow> (t,n)}" |
|
84 |
||
85 |
definition |
|
86 |
"linked_list_init = |
|
87 |
WHILE Less (!(N 1)) (!(N 0)) |
|
88 |
DO ( New (N 3) (N 2); |
|
89 |
N 1 ::= Plus (!(N 1)) (N 1); |
|
90 |
!(N 3) ::= !(N 1); |
|
91 |
Plus (!(N 3)) (N 1) ::= !(N 2); |
|
92 |
N 2 ::= !(N 3) )" |
|
93 |
||
94 |
values "{list t n |t n. (linked_list_init, nth[2,0,0,0],4) \<Rightarrow> (t,n)}" |
|
95 |
||
96 |
end |