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

src/HOL/Isar_Examples/Expr_Compiler.thy

author | nipkow |

Mon Jan 30 21:49:41 2012 +0100 (2012-01-30) | |

changeset 46372 | 6fa9cdb8b850 |

parent 41818 | 6d4c3ee8219d |

child 46582 | dcc312f22ee8 |

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

added "'a rel"

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 => 'val => '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 ('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 => ('adr => 'val) => '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 ('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

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

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

65 where

66 "exec [] stack env = stack"

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

68 (case instr of

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

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

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

72 # (tl (tl stack))) env)"

74 definition

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

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

79 subsection {* Compiler *}

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

82 to lists of stack machine instructions. *}

84 primrec

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

86 where

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

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

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

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

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

94 and list append. *}

96 lemma exec_append:

97 "exec (xs @ ys) stack env =

98 exec ys (exec xs stack env) env"

99 proof (induct xs arbitrary: stack)

100 case Nil

101 show ?case by simp

102 next

103 case (Cons x xs)

104 show ?case

105 proof (induct x)

106 case Const

107 from Cons show ?case by simp

108 next

109 case Load

110 from Cons show ?case by simp

111 next

112 case Apply

113 from Cons show ?case by simp

114 qed

115 qed

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

118 proof -

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

120 proof (induct e)

121 case Variable show ?case by simp

122 next

123 case Constant show ?case by simp

124 next

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

126 qed

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

128 qed

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

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

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

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

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

137 lemma exec_append':

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

139 proof (induct xs arbitrary: stack)

140 case (Nil s)

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

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

143 finally show ?case .

144 next

145 case (Cons x xs s)

146 show ?case

147 proof (induct x)

148 case (Const val)

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

150 by simp

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

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

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

154 finally show ?case .

155 next

156 case (Load adr)

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

158 next

159 case (Apply fn)

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

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

162 also have "... =

163 exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env" by simp

164 also from Cons have "... =

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

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

167 finally show ?case .

168 qed

169 qed

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

172 proof -

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

174 proof (induct e)

175 case (Variable adr s)

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

177 by simp

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

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

180 finally show ?case .

181 next

182 case (Constant val s)

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

184 next

185 case (Binop fn e1 e2 s)

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

187 exec (compile e2 @ compile e1 @ [Apply fn]) s env" by simp

188 also have "... = exec [Apply fn]

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

190 by (simp only: exec_append)

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

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

193 also have "exec [Apply fn] ... env =

194 fn (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp

195 also have "... = fn (eval e1 env) (eval e2 env) # s" by simp

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

197 eval (Binop fn e1 e2) env"

198 by simp

199 finally show ?case .

200 qed

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

203 by (simp add: execute_def)

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

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

206 finally show ?thesis .

207 qed

209 end