31 |
31 |
32 |
32 |
33 section \<open>A polymorphic heap inside a monad\<close> |
33 section \<open>A polymorphic heap inside a monad\<close> |
34 |
34 |
35 text \<open> |
35 text \<open> |
36 Heaps (@{type heap}) can be populated by values of class @{class |
36 Heaps (\<^type>\<open>heap\<close>) can be populated by values of class \<^class>\<open>heap\<close>; HOL's default types are already instantiated to class \<^class>\<open>heap\<close>. Class \<^class>\<open>heap\<close> is a subclass of \<^class>\<open>countable\<close>; see |
37 heap}; HOL's default types are already instantiated to class @{class |
37 theory \<open>Countable\<close> for ways to instantiate types as \<^class>\<open>countable\<close>. |
38 heap}. Class @{class heap} is a subclass of @{class countable}; see |
38 |
39 theory \<open>Countable\<close> for ways to instantiate types as @{class countable}. |
39 The heap is wrapped up in a monad \<^typ>\<open>'a Heap\<close> by means of the |
40 |
|
41 The heap is wrapped up in a monad @{typ "'a Heap"} by means of the |
|
42 following specification: |
40 following specification: |
43 |
41 |
44 \begin{quote} |
42 \begin{quote} |
45 @{datatype Heap} |
43 \<^datatype>\<open>Heap\<close> |
46 \end{quote} |
44 \end{quote} |
47 |
45 |
48 Unwrapping of this monad type happens through |
46 Unwrapping of this monad type happens through |
49 |
47 |
50 \begin{quote} |
48 \begin{quote} |
51 @{term_type execute} \\ |
49 \<^term_type>\<open>execute\<close> \\ |
52 @{thm execute.simps [no_vars]} |
50 @{thm execute.simps [no_vars]} |
53 \end{quote} |
51 \end{quote} |
54 |
52 |
55 This allows for equational reasoning about monadic expressions; the |
53 This allows for equational reasoning about monadic expressions; the |
56 fact collection \<open>execute_simps\<close> contains appropriate rewrites |
54 fact collection \<open>execute_simps\<close> contains appropriate rewrites |
64 \end{quote} |
62 \end{quote} |
65 |
63 |
66 Monadic expression involve the usual combinators: |
64 Monadic expression involve the usual combinators: |
67 |
65 |
68 \begin{quote} |
66 \begin{quote} |
69 @{term_type return} \\ |
67 \<^term_type>\<open>return\<close> \\ |
70 @{term_type bind} \\ |
68 \<^term_type>\<open>bind\<close> \\ |
71 @{term_type raise} |
69 \<^term_type>\<open>raise\<close> |
72 \end{quote} |
70 \end{quote} |
73 |
71 |
74 This is also associated with nice monad do-syntax. The @{typ |
72 This is also associated with nice monad do-syntax. The \<^typ>\<open>string\<close> argument to \<^const>\<open>raise\<close> is just a codified comment. |
75 string} argument to @{const raise} is just a codified comment. |
|
76 |
73 |
77 Among a couple of generic combinators the following is helpful for |
74 Among a couple of generic combinators the following is helpful for |
78 establishing invariants: |
75 establishing invariants: |
79 |
76 |
80 \begin{quote} |
77 \begin{quote} |
81 @{term_type assert} \\ |
78 \<^term_type>\<open>assert\<close> \\ |
82 @{thm assert_def [no_vars]} |
79 @{thm assert_def [no_vars]} |
83 \end{quote} |
80 \end{quote} |
84 \<close> |
81 \<close> |
85 |
82 |
86 |
83 |
87 section \<open>Relational reasoning about @{type Heap} expressions\<close> |
84 section \<open>Relational reasoning about \<^type>\<open>Heap\<close> expressions\<close> |
88 |
85 |
89 text \<open> |
86 text \<open> |
90 To establish correctness of imperative programs, predicate |
87 To establish correctness of imperative programs, predicate |
91 |
88 |
92 \begin{quote} |
89 \begin{quote} |
93 @{term_type effect} |
90 \<^term_type>\<open>effect\<close> |
94 \end{quote} |
91 \end{quote} |
95 |
92 |
96 provides a simple relational calculus. Primitive rules are \<open>effectI\<close> and \<open>effectE\<close>, rules appropriate for reasoning about |
93 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 |
94 imperative operations are available in the \<open>effect_intros\<close> and |
98 \<open>effect_elims\<close> fact collections. |
95 \<open>effect_elims\<close> fact collections. |
99 |
96 |
100 Often non-failure of imperative computations does not depend |
97 Often non-failure of imperative computations does not depend |
101 on the heap at all; reasoning then can be easier using predicate |
98 on the heap at all; reasoning then can be easier using predicate |
102 |
99 |
103 \begin{quote} |
100 \begin{quote} |
104 @{term_type success} |
101 \<^term_type>\<open>success\<close> |
105 \end{quote} |
102 \end{quote} |
106 |
103 |
107 Introduction rules for @{const success} are available in the |
104 Introduction rules for \<^const>\<open>success\<close> are available in the |
108 \<open>success_intro\<close> fact collection. |
105 \<open>success_intro\<close> fact collection. |
109 |
106 |
110 @{const execute}, @{const effect}, @{const success} and @{const bind} |
107 \<^const>\<open>execute\<close>, \<^const>\<open>effect\<close>, \<^const>\<open>success\<close> and \<^const>\<open>bind\<close> |
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>. |
108 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> |
109 \<close> |
113 |
110 |
114 |
111 |
115 section \<open>Monadic data structures\<close> |
112 section \<open>Monadic data structures\<close> |
139 |
136 |
140 text \<open> |
137 text \<open> |
141 Heap operations: |
138 Heap operations: |
142 |
139 |
143 \begin{quote} |
140 \begin{quote} |
144 @{term_type Array.alloc} \\ |
141 \<^term_type>\<open>Array.alloc\<close> \\ |
145 @{term_type Array.present} \\ |
142 \<^term_type>\<open>Array.present\<close> \\ |
146 @{term_type Array.get} \\ |
143 \<^term_type>\<open>Array.get\<close> \\ |
147 @{term_type Array.set} \\ |
144 \<^term_type>\<open>Array.set\<close> \\ |
148 @{term_type Array.length} \\ |
145 \<^term_type>\<open>Array.length\<close> \\ |
149 @{term_type Array.update} \\ |
146 \<^term_type>\<open>Array.update\<close> \\ |
150 @{term_type Array.noteq} |
147 \<^term_type>\<open>Array.noteq\<close> |
151 \end{quote} |
148 \end{quote} |
152 |
149 |
153 Monad operations: |
150 Monad operations: |
154 |
151 |
155 \begin{quote} |
152 \begin{quote} |
156 @{term_type Array.new} \\ |
153 \<^term_type>\<open>Array.new\<close> \\ |
157 @{term_type Array.of_list} \\ |
154 \<^term_type>\<open>Array.of_list\<close> \\ |
158 @{term_type Array.make} \\ |
155 \<^term_type>\<open>Array.make\<close> \\ |
159 @{term_type Array.len} \\ |
156 \<^term_type>\<open>Array.len\<close> \\ |
160 @{term_type Array.nth} \\ |
157 \<^term_type>\<open>Array.nth\<close> \\ |
161 @{term_type Array.upd} \\ |
158 \<^term_type>\<open>Array.upd\<close> \\ |
162 @{term_type Array.map_entry} \\ |
159 \<^term_type>\<open>Array.map_entry\<close> \\ |
163 @{term_type Array.swap} \\ |
160 \<^term_type>\<open>Array.swap\<close> \\ |
164 @{term_type Array.freeze} |
161 \<^term_type>\<open>Array.freeze\<close> |
165 \end{quote} |
162 \end{quote} |
166 \<close> |
163 \<close> |
167 |
164 |
168 subsection \<open>References\<close> |
165 subsection \<open>References\<close> |
169 |
166 |
170 text \<open> |
167 text \<open> |
171 Heap operations: |
168 Heap operations: |
172 |
169 |
173 \begin{quote} |
170 \begin{quote} |
174 @{term_type Ref.alloc} \\ |
171 \<^term_type>\<open>Ref.alloc\<close> \\ |
175 @{term_type Ref.present} \\ |
172 \<^term_type>\<open>Ref.present\<close> \\ |
176 @{term_type Ref.get} \\ |
173 \<^term_type>\<open>Ref.get\<close> \\ |
177 @{term_type Ref.set} \\ |
174 \<^term_type>\<open>Ref.set\<close> \\ |
178 @{term_type Ref.noteq} |
175 \<^term_type>\<open>Ref.noteq\<close> |
179 \end{quote} |
176 \end{quote} |
180 |
177 |
181 Monad operations: |
178 Monad operations: |
182 |
179 |
183 \begin{quote} |
180 \begin{quote} |
184 @{term_type Ref.ref} \\ |
181 \<^term_type>\<open>Ref.ref\<close> \\ |
185 @{term_type Ref.lookup} \\ |
182 \<^term_type>\<open>Ref.lookup\<close> \\ |
186 @{term_type Ref.update} \\ |
183 \<^term_type>\<open>Ref.update\<close> \\ |
187 @{term_type Ref.change} |
184 \<^term_type>\<open>Ref.change\<close> |
188 \end{quote} |
185 \end{quote} |
189 \<close> |
186 \<close> |
190 |
187 |
191 |
188 |
192 section \<open>Code generation\<close> |
189 section \<open>Code generation\<close> |