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