summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_examples/ExprCompiler.thy

author | obua |

Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) | |

changeset 19404 | 9bf2cdc9e8e8 |

parent 18193 | 54419506df9e |

child 20503 | 503ac4c5ef91 |

permissions | -rw-r--r-- |

Moved stuff from Ring_and_Field to Matrix

1 (* Title: HOL/Isar_examples/ExprCompiler.thy

2 ID: $Id$

3 Author: Markus Wenzel, TU Muenchen

5 Correctness of a simple expression/stack-machine compiler.

6 *)

8 header {* Correctness of a simple expression compiler *}

10 theory ExprCompiler imports Main begin

12 text {*

13 This is a (rather trivial) example of program verification. We model

14 a compiler for translating expressions to stack machine instructions,

15 and prove its correctness wrt.\ some evaluation semantics.

16 *}

19 subsection {* Binary operations *}

21 text {*

22 Binary operations are just functions over some type of values. This

23 is both for abstract syntax and semantics, i.e.\ we use a ``shallow

24 embedding'' here.

25 *}

27 types

28 'val binop = "'val => 'val => 'val"

31 subsection {* Expressions *}

33 text {*

34 The language of expressions is defined as an inductive type,

35 consisting of variables, constants, and binary operations on

36 expressions.

37 *}

39 datatype ('adr, 'val) expr =

40 Variable 'adr |

41 Constant 'val |

42 Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"

44 text {*

45 Evaluation (wrt.\ some environment of variable assignments) is

46 defined by primitive recursion over the structure of expressions.

47 *}

49 consts

50 eval :: "('adr, 'val) expr => ('adr => 'val) => 'val"

52 primrec

53 "eval (Variable x) env = env x"

54 "eval (Constant c) env = c"

55 "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"

58 subsection {* Machine *}

60 text {*

61 Next we model a simple stack machine, with three instructions.

62 *}

64 datatype ('adr, 'val) instr =

65 Const 'val |

66 Load 'adr |

67 Apply "'val binop"

69 text {*

70 Execution of a list of stack machine instructions is easily defined

71 as follows.

72 *}

74 consts

75 exec :: "(('adr, 'val) instr) list

76 => 'val list => ('adr => 'val) => 'val list"

78 primrec

79 "exec [] stack env = stack"

80 "exec (instr # instrs) stack env =

81 (case instr of

82 Const c => exec instrs (c # stack) env

83 | Load x => exec instrs (env x # stack) env

84 | Apply f => exec instrs (f (hd stack) (hd (tl stack))

85 # (tl (tl stack))) env)"

87 constdefs

88 execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"

89 "execute instrs env == hd (exec instrs [] env)"

92 subsection {* Compiler *}

94 text {*

95 We are ready to define the compilation function of expressions to

96 lists of stack machine instructions.

97 *}

99 consts

100 compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"

102 primrec

103 "compile (Variable x) = [Load x]"

104 "compile (Constant c) = [Const c]"

105 "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"

108 text {*

109 The main result of this development is the correctness theorem for

110 $\idt{compile}$. We first establish a lemma about $\idt{exec}$ and

111 list append.

112 *}

114 lemma exec_append:

115 "exec (xs @ ys) stack env =

116 exec ys (exec xs stack env) env"

117 proof (induct xs fixing: stack)

118 case Nil

119 show ?case by simp

120 next

121 case (Cons x xs)

122 show ?case

123 proof (induct x)

124 case Const show ?case by simp

125 next

126 case Load show ?case by simp

127 next

128 case Apply show ?case by simp

129 qed

130 qed

132 theorem correctness: "execute (compile e) env = eval e env"

133 proof -

134 have "\<And>stack. exec (compile e) stack env = eval e env # stack"

135 proof (induct e)

136 case Variable show ?case by simp

137 next

138 case Constant show ?case by simp

139 next

140 case Binop then show ?case by (simp add: exec_append)

141 qed

142 thus ?thesis by (simp add: execute_def)

143 qed

146 text {*

147 \bigskip In the proofs above, the \name{simp} method does quite a lot

148 of work behind the scenes (mostly ``functional program execution'').

149 Subsequently, the same reasoning is elaborated in detail --- at most

150 one recursive function definition is used at a time. Thus we get a

151 better idea of what is actually going on.

152 *}

154 lemma exec_append':

155 "exec (xs @ ys) stack env = exec ys (exec xs stack env) env"

156 proof (induct xs fixing: stack)

157 case (Nil s)

158 have "exec ([] @ ys) s env = exec ys s env" by simp

159 also have "... = exec ys (exec [] s env) env" by simp

160 finally show ?case .

161 next

162 case (Cons x xs s)

163 show ?case

164 proof (induct x)

165 case (Const val)

166 have "exec ((Const val # xs) @ ys) s env = exec (Const val # xs @ ys) s env"

167 by simp

168 also have "... = exec (xs @ ys) (val # s) env" by simp

169 also from Cons have "... = exec ys (exec xs (val # s) env) env" .

170 also have "... = exec ys (exec (Const val # xs) s env) env" by simp

171 finally show ?case .

172 next

173 case (Load adr)

174 from Cons show ?case by simp -- {* same as above *}

175 next

176 case (Apply fun)

177 have "exec ((Apply fun # xs) @ ys) s env =

178 exec (Apply fun # xs @ ys) s env" by simp

179 also have "... =

180 exec (xs @ ys) (fun (hd s) (hd (tl s)) # (tl (tl s))) env" by simp

181 also from Cons have "... =

182 exec ys (exec xs (fun (hd s) (hd (tl s)) # tl (tl s)) env) env" .

183 also have "... = exec ys (exec (Apply fun # xs) s env) env" by simp

184 finally show ?case .

185 qed

186 qed

188 theorem correctness': "execute (compile e) env = eval e env"

189 proof -

190 have exec_compile: "\<And>stack. exec (compile e) stack env = eval e env # stack"

191 proof (induct e)

192 case (Variable adr s)

193 have "exec (compile (Variable adr)) s env = exec [Load adr] s env"

194 by simp

195 also have "... = env adr # s" by simp

196 also have "env adr = eval (Variable adr) env" by simp

197 finally show ?case .

198 next

199 case (Constant val s)

200 show ?case by simp -- {* same as above *}

201 next

202 case (Binop fun e1 e2 s)

203 have "exec (compile (Binop fun e1 e2)) s env =

204 exec (compile e2 @ compile e1 @ [Apply fun]) s env" by simp

205 also have "... = exec [Apply fun]

206 (exec (compile e1) (exec (compile e2) s env) env) env"

207 by (simp only: exec_append)

208 also have "exec (compile e2) s env = eval e2 env # s" by fact

209 also have "exec (compile e1) ... env = eval e1 env # ..." by fact

210 also have "exec [Apply fun] ... env =

211 fun (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp

212 also have "... = fun (eval e1 env) (eval e2 env) # s" by simp

213 also have "fun (eval e1 env) (eval e2 env) =

214 eval (Binop fun e1 e2) env"

215 by simp

216 finally show ?case .

217 qed

219 have "execute (compile e) env = hd (exec (compile e) [] env)"

220 by (simp add: execute_def)

221 also from exec_compile

222 have "exec (compile e) [] env = [eval e env]" .

223 also have "hd ... = eval e env" by simp

224 finally show ?thesis .

225 qed

227 end