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

src/HOL/Isar_Examples/Expr_Compiler.thy

author | blanchet |

Tue Sep 09 20:51:36 2014 +0200 (2014-09-09) | |

changeset 58249 | 180f1b3508ed |

parent 55640 | abc140f21caa |

child 58260 | c96e511bfb79 |

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

use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries

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 {* This is a (rather trivial) example of program verification.

14 We model a compiler for translating expressions to stack machine

15 instructions, and prove its correctness wrt.\ some evaluation

16 semantics. *}

19 subsection {* Binary operations *}

21 text {* Binary operations are just functions over some type of values.

22 This is both for abstract syntax and semantics, i.e.\ we use a

23 ``shallow embedding'' here. *}

25 type_synonym 'val binop = "'val \<Rightarrow> 'val \<Rightarrow> 'val"

28 subsection {* Expressions *}

30 text {* The language of expressions is defined as an inductive type,

31 consisting of variables, constants, and binary operations on

32 expressions. *}

34 datatype_new ('adr, 'val) expr =

35 Variable 'adr

36 | Constant 'val

37 | Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"

39 text {* Evaluation (wrt.\ some environment of variable assignments) is

40 defined by primitive recursion over the structure of expressions. *}

42 primrec eval :: "('adr, 'val) expr \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"

43 where

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

45 | "eval (Constant c) env = c"

46 | "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"

49 subsection {* Machine *}

51 text {* Next we model a simple stack machine, with three

52 instructions. *}

54 datatype_new ('adr, 'val) instr =

55 Const 'val

56 | Load 'adr

57 | Apply "'val binop"

59 text {* Execution of a list of stack machine instructions is easily

60 defined as follows. *}

62 primrec exec :: "(('adr, 'val) instr) list \<Rightarrow> 'val list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val list"

63 where

64 "exec [] stack env = stack"

65 | "exec (instr # instrs) stack env =

66 (case instr of

67 Const c \<Rightarrow> exec instrs (c # stack) env

68 | Load x \<Rightarrow> exec instrs (env x # stack) env

69 | Apply f \<Rightarrow> exec instrs (f (hd stack) (hd (tl stack))

70 # (tl (tl stack))) env)"

72 definition execute :: "(('adr, 'val) instr) list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"

73 where "execute instrs env = hd (exec instrs [] env)"

76 subsection {* Compiler *}

78 text {* We are ready to define the compilation function of expressions

79 to lists of stack machine instructions. *}

81 primrec compile :: "('adr, 'val) expr \<Rightarrow> (('adr, 'val) instr) list"

82 where

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

84 | "compile (Constant c) = [Const c]"

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

88 text {* The main result of this development is the correctness theorem

89 for @{text compile}. We first establish a lemma about @{text exec}

90 and list append. *}

92 lemma exec_append:

93 "exec (xs @ ys) stack env =

94 exec ys (exec xs stack env) env"

95 proof (induct xs arbitrary: stack)

96 case Nil

97 show ?case by simp

98 next

99 case (Cons x xs)

100 show ?case

101 proof (induct x)

102 case Const

103 from Cons show ?case by simp

104 next

105 case Load

106 from Cons show ?case by simp

107 next

108 case Apply

109 from Cons show ?case by simp

110 qed

111 qed

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

114 proof -

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

116 proof (induct e)

117 case Variable

118 show ?case by simp

119 next

120 case Constant

121 show ?case by simp

122 next

123 case Binop

124 then show ?case by (simp add: exec_append)

125 qed

126 then show ?thesis by (simp add: execute_def)

127 qed

130 text {* \bigskip In the proofs above, the @{text simp} method does

131 quite a lot of work behind the scenes (mostly ``functional program

132 execution''). Subsequently, the same reasoning is elaborated in

133 detail --- at most one recursive function definition is used at a

134 time. Thus we get a better idea of what is actually going on. *}

136 lemma exec_append':

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

138 proof (induct xs arbitrary: stack)

139 case (Nil s)

140 have "exec ([] @ ys) s env = exec ys s env"

141 by simp

142 also have "\<dots> = exec ys (exec [] s env) env"

143 by simp

144 finally show ?case .

145 next

146 case (Cons x xs s)

147 show ?case

148 proof (induct x)

149 case (Const val)

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

151 by simp

152 also have "\<dots> = exec (xs @ ys) (val # s) env"

153 by simp

154 also from Cons have "\<dots> = exec ys (exec xs (val # s) env) env" .

155 also have "\<dots> = exec ys (exec (Const val # xs) s env) env"

156 by simp

157 finally show ?case .

158 next

159 case (Load adr)

160 from Cons show ?case

161 by simp -- {* same as above *}

162 next

163 case (Apply fn)

164 have "exec ((Apply fn # xs) @ ys) s env =

165 exec (Apply fn # xs @ ys) s env" by simp

166 also have "\<dots> =

167 exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env"

168 by simp

169 also from Cons have "\<dots> =

170 exec ys (exec xs (fn (hd s) (hd (tl s)) # tl (tl s)) env) env" .

171 also have "\<dots> = exec ys (exec (Apply fn # xs) s env) env"

172 by simp

173 finally show ?case .

174 qed

175 qed

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

178 proof -

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

180 proof (induct e)

181 case (Variable adr s)

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

183 by simp

184 also have "\<dots> = env adr # s"

185 by simp

186 also have "env adr = eval (Variable adr) env"

187 by simp

188 finally show ?case .

189 next

190 case (Constant val s)

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

192 next

193 case (Binop fn e1 e2 s)

194 have "exec (compile (Binop fn e1 e2)) s env =

195 exec (compile e2 @ compile e1 @ [Apply fn]) s env"

196 by simp

197 also have "\<dots> = exec [Apply fn]

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

199 by (simp only: exec_append)

200 also have "exec (compile e2) s env = eval e2 env # s"

201 by fact

202 also have "exec (compile e1) \<dots> env = eval e1 env # \<dots>"

203 by fact

204 also have "exec [Apply fn] \<dots> env =

205 fn (hd \<dots>) (hd (tl \<dots>)) # (tl (tl \<dots>))"

206 by simp

207 also have "\<dots> = fn (eval e1 env) (eval e2 env) # s"

208 by simp

209 also have "fn (eval e1 env) (eval e2 env) =

210 eval (Binop fn e1 e2) env"

211 by simp

212 finally show ?case .

213 qed

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

216 by (simp add: execute_def)

217 also from exec_compile have "exec (compile e) [] env = [eval e env]" .

218 also have "hd \<dots> = eval e env"

219 by simp

220 finally show ?thesis .

221 qed

223 end