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

src/HOL/Isar_examples/ExprCompiler.thy

author | oheimb |

Wed Jan 31 10:15:55 2001 +0100 (2001-01-31) | |

changeset 11008 | f7333f055ef6 |

parent 10007 | 64bf7da1994a |

child 11809 | c9ffdd63dd93 |

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

improved theory reference in comment

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 = Main:

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 "ALL stack. exec (xs @ ys) stack env =

116 exec ys (exec xs stack env) env" (is "?P xs")

117 proof (induct ?P xs type: list)

118 show "?P []" by simp

120 fix x xs assume "?P xs"

121 show "?P (x # xs)" (is "?Q x")

122 proof (induct ?Q x type: instr)

123 show "!!val. ?Q (Const val)" by (simp!)

124 show "!!adr. ?Q (Load adr)" by (simp!)

125 show "!!fun. ?Q (Apply fun)" by (simp!)

126 qed

127 qed

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

130 proof -

131 have "ALL stack. exec (compile e) stack env =

132 eval e env # stack" (is "?P e")

133 proof (induct ?P e type: expr)

134 show "!!adr. ?P (Variable adr)" by simp

135 show "!!val. ?P (Constant val)" by simp

136 show "!!fun e1 e2. (?P e1 ==> ?P e2 ==> ?P (Binop fun e1 e2))"

137 by (simp add: exec_append)

138 qed

139 thus ?thesis by (simp add: execute_def)

140 qed

143 text {*

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

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

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

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

148 better idea of what is actually going on.

149 *}

151 lemma exec_append:

152 "ALL stack. exec (xs @ ys) stack env

153 = exec ys (exec xs stack env) env" (is "?P xs")

154 proof (induct ?P xs)

155 show "?P []" (is "ALL s. ?Q s")

156 proof

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

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

159 finally show "?Q s" .

160 qed

161 fix x xs assume hyp: "?P xs"

162 show "?P (x # xs)"

163 proof (induct x)

164 fix val

165 show "?P (Const val # xs)" (is "ALL s. ?Q s")

166 proof

167 fix s

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

169 exec (Const val # xs @ ys) s env"

170 by simp

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

172 also from hyp

173 have "... = exec ys (exec xs (val # s) env) env" ..

174 also have "... = exec ys (exec (Const val # xs) s env) env"

175 by simp

176 finally show "?Q s" .

177 qed

178 next

179 fix adr from hyp show "?P (Load adr # xs)" by simp -- {* same as above *}

180 next

181 fix fun

182 show "?P (Apply fun # xs)" (is "ALL s. ?Q s")

183 proof

184 fix s

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

186 exec (Apply fun # xs @ ys) s env"

187 by simp

188 also have "... =

189 exec (xs @ ys) (fun (hd s) (hd (tl s)) # (tl (tl s))) env"

190 by simp

191 also from hyp have "... =

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

193 ..

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

195 finally show "?Q s" .

196 qed

197 qed

198 qed

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

201 proof -

202 have exec_compile:

203 "ALL stack. exec (compile e) stack env = eval e env # stack"

204 (is "?P e")

205 proof (induct e)

206 fix adr show "?P (Variable adr)" (is "ALL s. ?Q s")

207 proof

208 fix s

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

210 by simp

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

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

213 finally show "?Q s" .

214 qed

215 next

216 fix val show "?P (Constant val)" by simp -- {* same as above *}

217 next

218 fix fun e1 e2 assume hyp1: "?P e1" and hyp2: "?P e2"

219 show "?P (Binop fun e1 e2)" (is "ALL s. ?Q s")

220 proof

221 fix s have "exec (compile (Binop fun e1 e2)) s env

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

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

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

225 by (simp only: exec_append)

226 also from hyp2

227 have "exec (compile e2) s env = eval e2 env # s" ..

228 also from hyp1

229 have "exec (compile e1) ... env = eval e1 env # ..." ..

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

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

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

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

234 eval (Binop fun e1 e2) env"

235 by simp

236 finally show "?Q s" .

237 qed

238 qed

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

241 by (simp add: execute_def)

242 also from exec_compile

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

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

245 finally show ?thesis .

246 qed

248 end