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

src/HOL/Isar_Examples/Expr_Compiler.thy

author | wenzelm |

Tue Oct 20 19:37:09 2009 +0200 (2009-10-20) | |

changeset 33026 | 8f35633c4922 |

parent 31758 | src/HOL/Isar_examples/Expr_Compiler.thy@3edd5f813f01 |

child 35416 | d8d7d1b785af |

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

modernized session Isar_Examples;

1 (* Title: HOL/Isar_Examples/Expr_Compiler.thy

2 Author: Markus Wenzel, TU Muenchen

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

5 *)

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

9 theory Expr_Compiler

10 imports Main

11 begin

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 *}

20 subsection {* Binary operations *}

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 *}

28 types

29 'val binop = "'val => 'val => 'val"

32 subsection {* Expressions *}

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 *}

40 datatype ('adr, 'val) expr =

41 Variable 'adr |

42 Constant 'val |

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

45 text {*

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

47 defined by primitive recursion over the structure of expressions.

48 *}

50 consts

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

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)"

59 subsection {* Machine *}

61 text {*

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

63 *}

65 datatype ('adr, 'val) instr =

66 Const 'val |

67 Load 'adr |

68 Apply "'val binop"

70 text {*

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

72 as follows.

73 *}

75 consts

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

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

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)"

88 constdefs

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

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

93 subsection {* Compiler *}

95 text {*

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

97 lists of stack machine instructions.

98 *}

100 consts

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

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]"

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 *}

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

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

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 *}

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

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

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

231 end