author | paulson |
Thu, 14 Jun 2018 14:23:48 +0100 | |
changeset 68446 | 92ddca1edc43 |
parent 66453 | cc19f7ca2ed6 |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
39307 | 1 |
(* Title: HOL/Imperative_HOL/Overview.thy |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
(*<*) |
|
6 |
theory Overview |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63167
diff
changeset
|
7 |
imports Imperative_HOL "HOL-Library.LaTeXsugar" |
39307 | 8 |
begin |
9 |
||
10 |
(* type constraints with spacing *) |
|
61143 | 11 |
no_syntax (output) |
12 |
"_constrain" :: "logic => type => logic" ("_::_" [4, 0] 3) |
|
13 |
"_constrain" :: "prop' => type => prop'" ("_::_" [4, 0] 3) |
|
14 |
||
15 |
syntax (output) |
|
16 |
"_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3) |
|
17 |
"_constrain" :: "prop' => type => prop'" ("_ :: _" [4, 0] 3) |
|
18 |
(*>*) |
|
39307 | 19 |
|
63167 | 20 |
text \<open> |
21 |
\<open>Imperative HOL\<close> is a leightweight framework for reasoning |
|
22 |
about imperative data structures in \<open>Isabelle/HOL\<close> |
|
58622 | 23 |
@{cite "Nipkow-et-al:2002:tutorial"}. Its basic ideas are described in |
24 |
@{cite "Bulwahn-et-al:2008:imp_HOL"}. However their concrete |
|
39307 | 25 |
realisation has changed since, due to both extensions and |
26 |
refinements. Therefore this overview wants to present the framework |
|
27 |
\qt{as it is} by now. It focusses on the user-view, less on matters |
|
40358 | 28 |
of construction. For details study of the theory sources is |
39307 | 29 |
encouraged. |
63167 | 30 |
\<close> |
39307 | 31 |
|
32 |
||
63167 | 33 |
section \<open>A polymorphic heap inside a monad\<close> |
39307 | 34 |
|
63167 | 35 |
text \<open> |
39307 | 36 |
Heaps (@{type heap}) can be populated by values of class @{class |
37 |
heap}; HOL's default types are already instantiated to class @{class |
|
40358 | 38 |
heap}. Class @{class heap} is a subclass of @{class countable}; see |
63167 | 39 |
theory \<open>Countable\<close> for ways to instantiate types as @{class countable}. |
39307 | 40 |
|
41 |
The heap is wrapped up in a monad @{typ "'a Heap"} by means of the |
|
42 |
following specification: |
|
43 |
||
44 |
\begin{quote} |
|
45 |
@{datatype Heap} |
|
46 |
\end{quote} |
|
47 |
||
48 |
Unwrapping of this monad type happens through |
|
49 |
||
50 |
\begin{quote} |
|
51 |
@{term_type execute} \\ |
|
52 |
@{thm execute.simps [no_vars]} |
|
53 |
\end{quote} |
|
54 |
||
55 |
This allows for equational reasoning about monadic expressions; the |
|
63167 | 56 |
fact collection \<open>execute_simps\<close> contains appropriate rewrites |
39307 | 57 |
for all fundamental operations. |
58 |
||
39610 | 59 |
Primitive fine-granular control over heaps is available through rule |
63167 | 60 |
\<open>Heap_cases\<close>: |
39307 | 61 |
|
62 |
\begin{quote} |
|
63 |
@{thm [break] Heap_cases [no_vars]} |
|
64 |
\end{quote} |
|
65 |
||
66 |
Monadic expression involve the usual combinators: |
|
67 |
||
68 |
\begin{quote} |
|
69 |
@{term_type return} \\ |
|
70 |
@{term_type bind} \\ |
|
71 |
@{term_type raise} |
|
72 |
\end{quote} |
|
73 |
||
74 |
This is also associated with nice monad do-syntax. The @{typ |
|
75 |
string} argument to @{const raise} is just a codified comment. |
|
76 |
||
77 |
Among a couple of generic combinators the following is helpful for |
|
78 |
establishing invariants: |
|
79 |
||
80 |
\begin{quote} |
|
81 |
@{term_type assert} \\ |
|
82 |
@{thm assert_def [no_vars]} |
|
83 |
\end{quote} |
|
63167 | 84 |
\<close> |
39307 | 85 |
|
86 |
||
63167 | 87 |
section \<open>Relational reasoning about @{type Heap} expressions\<close> |
39307 | 88 |
|
63167 | 89 |
text \<open> |
39307 | 90 |
To establish correctness of imperative programs, predicate |
91 |
||
92 |
\begin{quote} |
|
40671 | 93 |
@{term_type effect} |
39307 | 94 |
\end{quote} |
95 |
||
63167 | 96 |
provides a simple relational calculus. Primitive rules are \<open>effectI\<close> and \<open>effectE\<close>, rules appropriate for reasoning about |
97 |
imperative operations are available in the \<open>effect_intros\<close> and |
|
98 |
\<open>effect_elims\<close> fact collections. |
|
39307 | 99 |
|
100 |
Often non-failure of imperative computations does not depend |
|
101 |
on the heap at all; reasoning then can be easier using predicate |
|
102 |
||
103 |
\begin{quote} |
|
104 |
@{term_type success} |
|
105 |
\end{quote} |
|
106 |
||
107 |
Introduction rules for @{const success} are available in the |
|
63167 | 108 |
\<open>success_intro\<close> fact collection. |
39307 | 109 |
|
40671 | 110 |
@{const execute}, @{const effect}, @{const success} and @{const bind} |
63167 | 111 |
are related by rules \<open>execute_bind_success\<close>, \<open>success_bind_executeI\<close>, \<open>success_bind_effectI\<close>, \<open>effect_bindI\<close>, \<open>effect_bindE\<close> and \<open>execute_bind_eq_SomeI\<close>. |
112 |
\<close> |
|
39307 | 113 |
|
114 |
||
63167 | 115 |
section \<open>Monadic data structures\<close> |
39307 | 116 |
|
63167 | 117 |
text \<open> |
39307 | 118 |
The operations for monadic data structures (arrays and references) |
119 |
come in two flavours: |
|
120 |
||
121 |
\begin{itemize} |
|
122 |
||
123 |
\item Operations on the bare heap; their number is kept minimal |
|
124 |
to facilitate proving. |
|
125 |
||
126 |
\item Operations on the heap wrapped up in a monad; these are designed |
|
127 |
for executing. |
|
128 |
||
129 |
\end{itemize} |
|
130 |
||
131 |
Provided proof rules are such that they reduce monad operations to |
|
132 |
operations on bare heaps. |
|
39717 | 133 |
|
134 |
Note that HOL equality coincides with reference equality and may be |
|
135 |
used as primitive executable operation. |
|
63167 | 136 |
\<close> |
39307 | 137 |
|
63167 | 138 |
subsection \<open>Arrays\<close> |
39307 | 139 |
|
63167 | 140 |
text \<open> |
39307 | 141 |
Heap operations: |
142 |
||
143 |
\begin{quote} |
|
144 |
@{term_type Array.alloc} \\ |
|
145 |
@{term_type Array.present} \\ |
|
146 |
@{term_type Array.get} \\ |
|
147 |
@{term_type Array.set} \\ |
|
148 |
@{term_type Array.length} \\ |
|
149 |
@{term_type Array.update} \\ |
|
150 |
@{term_type Array.noteq} |
|
151 |
\end{quote} |
|
152 |
||
153 |
Monad operations: |
|
154 |
||
155 |
\begin{quote} |
|
156 |
@{term_type Array.new} \\ |
|
157 |
@{term_type Array.of_list} \\ |
|
158 |
@{term_type Array.make} \\ |
|
159 |
@{term_type Array.len} \\ |
|
160 |
@{term_type Array.nth} \\ |
|
161 |
@{term_type Array.upd} \\ |
|
162 |
@{term_type Array.map_entry} \\ |
|
163 |
@{term_type Array.swap} \\ |
|
164 |
@{term_type Array.freeze} |
|
165 |
\end{quote} |
|
63167 | 166 |
\<close> |
39307 | 167 |
|
63167 | 168 |
subsection \<open>References\<close> |
39307 | 169 |
|
63167 | 170 |
text \<open> |
39307 | 171 |
Heap operations: |
172 |
||
173 |
\begin{quote} |
|
174 |
@{term_type Ref.alloc} \\ |
|
175 |
@{term_type Ref.present} \\ |
|
176 |
@{term_type Ref.get} \\ |
|
177 |
@{term_type Ref.set} \\ |
|
178 |
@{term_type Ref.noteq} |
|
179 |
\end{quote} |
|
180 |
||
181 |
Monad operations: |
|
182 |
||
183 |
\begin{quote} |
|
184 |
@{term_type Ref.ref} \\ |
|
185 |
@{term_type Ref.lookup} \\ |
|
186 |
@{term_type Ref.update} \\ |
|
187 |
@{term_type Ref.change} |
|
188 |
\end{quote} |
|
63167 | 189 |
\<close> |
39307 | 190 |
|
191 |
||
63167 | 192 |
section \<open>Code generation\<close> |
39307 | 193 |
|
63167 | 194 |
text \<open> |
39307 | 195 |
Imperative HOL sets up the code generator in a way that imperative |
196 |
operations are mapped to suitable counterparts in the target |
|
63167 | 197 |
language. For \<open>Haskell\<close>, a suitable \<open>ST\<close> monad is used; |
198 |
for \<open>SML\<close>, \<open>Ocaml\<close> and \<open>Scala\<close> unit values ensure |
|
39307 | 199 |
that the evaluation order is the same as you would expect from the |
200 |
original monadic expressions. These units may look cumbersome; the |
|
63167 | 201 |
target language variants \<open>SML_imp\<close>, \<open>Ocaml_imp\<close> and |
202 |
\<open>Scala_imp\<close> make some effort to optimize some of them away. |
|
203 |
\<close> |
|
39307 | 204 |
|
205 |
||
63167 | 206 |
section \<open>Some hints for using the framework\<close> |
39307 | 207 |
|
63167 | 208 |
text \<open> |
39307 | 209 |
Of course a framework itself does not by itself indicate how to make |
210 |
best use of it. Here some hints drawn from prior experiences with |
|
211 |
Imperative HOL: |
|
212 |
||
213 |
\begin{itemize} |
|
214 |
||
215 |
\item Proofs on bare heaps should be strictly separated from those |
|
216 |
for monadic expressions. The first capture the essence, while the |
|
217 |
latter just describe a certain wrapping-up. |
|
218 |
||
219 |
\item A good methodology is to gradually improve an imperative |
|
220 |
program from a functional one. In the extreme case this means |
|
221 |
that an original functional program is decomposed into suitable |
|
222 |
operations with exactly one corresponding imperative operation. |
|
223 |
Having shown suitable correspondence lemmas between those, the |
|
224 |
correctness prove of the whole imperative program simply |
|
225 |
consists of composing those. |
|
226 |
||
227 |
\item Whether one should prefer equational reasoning (fact |
|
63167 | 228 |
collection \<open>execute_simps\<close> or relational reasoning (fact |
229 |
collections \<open>effect_intros\<close> and \<open>effect_elims\<close>) depends |
|
39610 | 230 |
on the problems to solve. For complex expressions or |
231 |
expressions involving binders, the relation style usually is |
|
232 |
superior but requires more proof text. |
|
39307 | 233 |
|
234 |
\item Note that you can extend the fact collections of Imperative |
|
39610 | 235 |
HOL yourself whenever appropriate. |
39307 | 236 |
|
237 |
\end{itemize} |
|
63167 | 238 |
\<close> |
39307 | 239 |
|
62390 | 240 |
end |