|
1 (* Title: HOL/Isar_examples/Expr_Compiler.thy |
|
2 Author: Markus Wenzel, TU Muenchen |
|
3 |
|
4 Correctness of a simple expression/stack-machine compiler. |
|
5 *) |
|
6 |
|
7 header {* Correctness of a simple expression compiler *} |
|
8 |
|
9 theory Expr_Compiler |
|
10 imports Main |
|
11 begin |
|
12 |
|
13 text {* |
|
14 This is a (rather trivial) example of program verification. We model |
|
15 a compiler for translating expressions to stack machine instructions, |
|
16 and prove its correctness wrt.\ some evaluation semantics. |
|
17 *} |
|
18 |
|
19 |
|
20 subsection {* Binary operations *} |
|
21 |
|
22 text {* |
|
23 Binary operations are just functions over some type of values. This |
|
24 is both for abstract syntax and semantics, i.e.\ we use a ``shallow |
|
25 embedding'' here. |
|
26 *} |
|
27 |
|
28 types |
|
29 'val binop = "'val => 'val => 'val" |
|
30 |
|
31 |
|
32 subsection {* Expressions *} |
|
33 |
|
34 text {* |
|
35 The language of expressions is defined as an inductive type, |
|
36 consisting of variables, constants, and binary operations on |
|
37 expressions. |
|
38 *} |
|
39 |
|
40 datatype ('adr, 'val) expr = |
|
41 Variable 'adr | |
|
42 Constant 'val | |
|
43 Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr" |
|
44 |
|
45 text {* |
|
46 Evaluation (wrt.\ some environment of variable assignments) is |
|
47 defined by primitive recursion over the structure of expressions. |
|
48 *} |
|
49 |
|
50 consts |
|
51 eval :: "('adr, 'val) expr => ('adr => 'val) => 'val" |
|
52 |
|
53 primrec |
|
54 "eval (Variable x) env = env x" |
|
55 "eval (Constant c) env = c" |
|
56 "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)" |
|
57 |
|
58 |
|
59 subsection {* Machine *} |
|
60 |
|
61 text {* |
|
62 Next we model a simple stack machine, with three instructions. |
|
63 *} |
|
64 |
|
65 datatype ('adr, 'val) instr = |
|
66 Const 'val | |
|
67 Load 'adr | |
|
68 Apply "'val binop" |
|
69 |
|
70 text {* |
|
71 Execution of a list of stack machine instructions is easily defined |
|
72 as follows. |
|
73 *} |
|
74 |
|
75 consts |
|
76 exec :: "(('adr, 'val) instr) list |
|
77 => 'val list => ('adr => 'val) => 'val list" |
|
78 |
|
79 primrec |
|
80 "exec [] stack env = stack" |
|
81 "exec (instr # instrs) stack env = |
|
82 (case instr of |
|
83 Const c => exec instrs (c # stack) env |
|
84 | Load x => exec instrs (env x # stack) env |
|
85 | Apply f => exec instrs (f (hd stack) (hd (tl stack)) |
|
86 # (tl (tl stack))) env)" |
|
87 |
|
88 constdefs |
|
89 execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val" |
|
90 "execute instrs env == hd (exec instrs [] env)" |
|
91 |
|
92 |
|
93 subsection {* Compiler *} |
|
94 |
|
95 text {* |
|
96 We are ready to define the compilation function of expressions to |
|
97 lists of stack machine instructions. |
|
98 *} |
|
99 |
|
100 consts |
|
101 compile :: "('adr, 'val) expr => (('adr, 'val) instr) list" |
|
102 |
|
103 primrec |
|
104 "compile (Variable x) = [Load x]" |
|
105 "compile (Constant c) = [Const c]" |
|
106 "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]" |
|
107 |
|
108 |
|
109 text {* |
|
110 The main result of this development is the correctness theorem for |
|
111 $\idt{compile}$. We first establish a lemma about $\idt{exec}$ and |
|
112 list append. |
|
113 *} |
|
114 |
|
115 lemma exec_append: |
|
116 "exec (xs @ ys) stack env = |
|
117 exec ys (exec xs stack env) env" |
|
118 proof (induct xs arbitrary: stack) |
|
119 case Nil |
|
120 show ?case by simp |
|
121 next |
|
122 case (Cons x xs) |
|
123 show ?case |
|
124 proof (induct x) |
|
125 case Const |
|
126 from Cons show ?case by simp |
|
127 next |
|
128 case Load |
|
129 from Cons show ?case by simp |
|
130 next |
|
131 case Apply |
|
132 from Cons show ?case by simp |
|
133 qed |
|
134 qed |
|
135 |
|
136 theorem correctness: "execute (compile e) env = eval e env" |
|
137 proof - |
|
138 have "\<And>stack. exec (compile e) stack env = eval e env # stack" |
|
139 proof (induct e) |
|
140 case Variable show ?case by simp |
|
141 next |
|
142 case Constant show ?case by simp |
|
143 next |
|
144 case Binop then show ?case by (simp add: exec_append) |
|
145 qed |
|
146 then show ?thesis by (simp add: execute_def) |
|
147 qed |
|
148 |
|
149 |
|
150 text {* |
|
151 \bigskip In the proofs above, the \name{simp} method does quite a lot |
|
152 of work behind the scenes (mostly ``functional program execution''). |
|
153 Subsequently, the same reasoning is elaborated in detail --- at most |
|
154 one recursive function definition is used at a time. Thus we get a |
|
155 better idea of what is actually going on. |
|
156 *} |
|
157 |
|
158 lemma exec_append': |
|
159 "exec (xs @ ys) stack env = exec ys (exec xs stack env) env" |
|
160 proof (induct xs arbitrary: stack) |
|
161 case (Nil s) |
|
162 have "exec ([] @ ys) s env = exec ys s env" by simp |
|
163 also have "... = exec ys (exec [] s env) env" by simp |
|
164 finally show ?case . |
|
165 next |
|
166 case (Cons x xs s) |
|
167 show ?case |
|
168 proof (induct x) |
|
169 case (Const val) |
|
170 have "exec ((Const val # xs) @ ys) s env = exec (Const val # xs @ ys) s env" |
|
171 by simp |
|
172 also have "... = exec (xs @ ys) (val # s) env" by simp |
|
173 also from Cons have "... = exec ys (exec xs (val # s) env) env" . |
|
174 also have "... = exec ys (exec (Const val # xs) s env) env" by simp |
|
175 finally show ?case . |
|
176 next |
|
177 case (Load adr) |
|
178 from Cons show ?case by simp -- {* same as above *} |
|
179 next |
|
180 case (Apply fn) |
|
181 have "exec ((Apply fn # xs) @ ys) s env = |
|
182 exec (Apply fn # xs @ ys) s env" by simp |
|
183 also have "... = |
|
184 exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env" by simp |
|
185 also from Cons have "... = |
|
186 exec ys (exec xs (fn (hd s) (hd (tl s)) # tl (tl s)) env) env" . |
|
187 also have "... = exec ys (exec (Apply fn # xs) s env) env" by simp |
|
188 finally show ?case . |
|
189 qed |
|
190 qed |
|
191 |
|
192 theorem correctness': "execute (compile e) env = eval e env" |
|
193 proof - |
|
194 have exec_compile: "\<And>stack. exec (compile e) stack env = eval e env # stack" |
|
195 proof (induct e) |
|
196 case (Variable adr s) |
|
197 have "exec (compile (Variable adr)) s env = exec [Load adr] s env" |
|
198 by simp |
|
199 also have "... = env adr # s" by simp |
|
200 also have "env adr = eval (Variable adr) env" by simp |
|
201 finally show ?case . |
|
202 next |
|
203 case (Constant val s) |
|
204 show ?case by simp -- {* same as above *} |
|
205 next |
|
206 case (Binop fn e1 e2 s) |
|
207 have "exec (compile (Binop fn e1 e2)) s env = |
|
208 exec (compile e2 @ compile e1 @ [Apply fn]) s env" by simp |
|
209 also have "... = exec [Apply fn] |
|
210 (exec (compile e1) (exec (compile e2) s env) env) env" |
|
211 by (simp only: exec_append) |
|
212 also have "exec (compile e2) s env = eval e2 env # s" by fact |
|
213 also have "exec (compile e1) ... env = eval e1 env # ..." by fact |
|
214 also have "exec [Apply fn] ... env = |
|
215 fn (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp |
|
216 also have "... = fn (eval e1 env) (eval e2 env) # s" by simp |
|
217 also have "fn (eval e1 env) (eval e2 env) = |
|
218 eval (Binop fn e1 e2) env" |
|
219 by simp |
|
220 finally show ?case . |
|
221 qed |
|
222 |
|
223 have "execute (compile e) env = hd (exec (compile e) [] env)" |
|
224 by (simp add: execute_def) |
|
225 also from exec_compile |
|
226 have "exec (compile e) [] env = [eval e env]" . |
|
227 also have "hd ... = eval e env" by simp |
|
228 finally show ?thesis . |
|
229 qed |
|
230 |
|
231 end |