author | wenzelm |
Fri, 18 Aug 2017 20:47:47 +0200 | |
changeset 66453 | cc19f7ca2ed6 |
parent 63167 | 0909deb8059b |
child 66992 | 69673025292e |
permissions | -rw-r--r-- |
45044 | 1 |
(*<*) |
2 |
theory Reference |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63167
diff
changeset
|
3 |
imports SPARK |
45044 | 4 |
begin |
5 |
||
6 |
syntax (my_constrain output) |
|
61143 | 7 |
"_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3) |
45044 | 8 |
(*>*) |
9 |
||
63167 | 10 |
chapter \<open>HOL-\SPARK{} Reference\<close> |
45044 | 11 |
|
63167 | 12 |
text \<open> |
45044 | 13 |
\label{sec:spark-reference} |
14 |
This section is intended as a quick reference for the HOL-\SPARK{} verification |
|
15 |
environment. In \secref{sec:spark-commands}, we give a summary of the commands |
|
16 |
provided by the HOL-\SPARK{}, while \secref{sec:spark-types} contains a description |
|
17 |
of how particular types of \SPARK{} and FDL are modelled in Isabelle. |
|
63167 | 18 |
\<close> |
45044 | 19 |
|
63167 | 20 |
section \<open>Commands\<close> |
45044 | 21 |
|
63167 | 22 |
text \<open> |
45044 | 23 |
\label{sec:spark-commands} |
24 |
This section describes the syntax and effect of each of the commands provided |
|
25 |
by HOL-\SPARK{}. |
|
59938 | 26 |
@{rail \<open> |
27 |
@'spark_open' name ('(' name ')')? |
|
28 |
\<close>} |
|
56798
939e88e79724
Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents:
48168
diff
changeset
|
29 |
Opens a new \SPARK{} verification environment and loads a \texttt{*.siv} file with VCs. |
939e88e79724
Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents:
48168
diff
changeset
|
30 |
Alternatively, \texttt{*.vcg} files can be loaded using \isa{\isacommand{spark\_open\_vcg}}. |
939e88e79724
Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents:
48168
diff
changeset
|
31 |
The corresponding \texttt{*.fdl} and \texttt{*.rls} |
45044 | 32 |
files must reside in the same directory as the file given as an argument to the command. |
33 |
This command also generates records and datatypes for the types specified in the |
|
34 |
\texttt{*.fdl} file, unless they have already been associated with user-defined |
|
35 |
Isabelle types (see below). |
|
36 |
Since the full package name currently cannot be determined from the files generated by the |
|
37 |
\SPARK{} Examiner, the command also allows to specify an optional package prefix in the |
|
38 |
format \texttt{$p_1$\_\_$\ldots$\_\_$p_n$}. When working with projects consisting of several |
|
39 |
packages, this is necessary in order for the verification environment to be able to map proof |
|
40 |
functions and types defined in Isabelle to their \SPARK{} counterparts. |
|
59938 | 41 |
@{rail \<open> |
42 |
@'spark_proof_functions' ((name '=' term)+) |
|
43 |
\<close>} |
|
45044 | 44 |
Associates a proof function with the given name to a term. The name should be the full name |
45 |
of the proof function as it appears in the \texttt{*.fdl} file, including the package prefix. |
|
46 |
This command can be used both inside and outside a verification environment. The latter |
|
47 |
variant is useful for introducing proof functions that are shared by several procedures |
|
48 |
or packages, whereas the former allows the given term to refer to the types generated |
|
49 |
by \isa{\isacommand{spark\_open}} for record or enumeration types specified in the |
|
50 |
\texttt{*.fdl} file. |
|
59938 | 51 |
@{rail \<open> |
52 |
@'spark_types' ((name '=' type (mapping?))+) |
|
53 |
; |
|
62969 | 54 |
mapping: '('((name '=' name)+',')')' |
59938 | 55 |
\<close>} |
45044 | 56 |
Associates a \SPARK{} type with the given name with an Isabelle type. This command can |
57 |
only be used outside a verification environment. The given type must be either a record |
|
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
45044
diff
changeset
|
58 |
or a datatype, where the names of fields or constructors must either match those of the |
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
45044
diff
changeset
|
59 |
corresponding \SPARK{} types (modulo casing), or a mapping from \SPARK{} to Isabelle |
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
45044
diff
changeset
|
60 |
names has to be provided. |
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
45044
diff
changeset
|
61 |
This command is useful when having to define |
45044 | 62 |
proof functions referring to record or enumeration types that are shared by several |
63 |
procedures or packages. First, the types required by the proof functions can be introduced |
|
64 |
using Isabelle's commands for defining records or datatypes. Having introduced the |
|
65 |
types, the proof functions can be defined in Isabelle. Finally, both the proof |
|
66 |
functions and the types can be associated with their \SPARK{} counterparts. |
|
59938 | 67 |
@{rail \<open> |
68 |
@'spark_status' (('(proved)' | '(unproved)')?) |
|
69 |
\<close>} |
|
45044 | 70 |
Outputs the variables declared in the \texttt{*.fdl} file, the rules declared in |
71 |
the \texttt{*.rls} file, and all VCs, together with their status (proved, unproved). |
|
72 |
The output can be restricted to the proved or unproved VCs by giving the corresponding |
|
73 |
option to the command. |
|
59938 | 74 |
@{rail \<open> |
75 |
@'spark_vc' name |
|
76 |
\<close>} |
|
45044 | 77 |
Initiates the proof of the VC with the given name. Similar to the standard |
78 |
\isa{\isacommand{lemma}} or \isa{\isacommand{theorem}} commands, this command |
|
79 |
must be followed by a sequence of proof commands. The command introduces the |
|
80 |
hypotheses \texttt{H1} \dots \texttt{H$n$}, as well as the identifiers |
|
81 |
\texttt{?C1} \dots \texttt{?C$m$} corresponding to the conclusions of the VC. |
|
59938 | 82 |
@{rail \<open> |
83 |
@'spark_end' '(incomplete)'? |
|
84 |
\<close>} |
|
48168 | 85 |
Closes the current verification environment. Unless the \texttt{incomplete} |
86 |
option is given, all VCs must have been proved, |
|
45044 | 87 |
otherwise the command issues an error message. As a side effect, the command |
88 |
generates a proof review (\texttt{*.prv}) file to inform POGS of the proved |
|
89 |
VCs. |
|
63167 | 90 |
\<close> |
45044 | 91 |
|
63167 | 92 |
section \<open>Types\<close> |
45044 | 93 |
|
63167 | 94 |
text \<open> |
45044 | 95 |
\label{sec:spark-types} |
96 |
The main types of FDL are integers, enumeration types, records, and arrays. |
|
97 |
In the following sections, we describe how these types are modelled in |
|
98 |
Isabelle. |
|
63167 | 99 |
\<close> |
45044 | 100 |
|
63167 | 101 |
subsection \<open>Integers\<close> |
45044 | 102 |
|
63167 | 103 |
text \<open> |
45044 | 104 |
The FDL type \texttt{integer} is modelled by the Isabelle type @{typ int}. |
105 |
While the FDL \texttt{mod} operator behaves in the same way as its Isabelle |
|
106 |
counterpart, this is not the case for the \texttt{div} operator. As has already |
|
107 |
been mentioned in \secref{sec:proving-vcs}, the \texttt{div} operator of \SPARK{} |
|
63167 | 108 |
always truncates towards zero, whereas the \<open>div\<close> operator of Isabelle |
45044 | 109 |
truncates towards minus infinity. Therefore, the FDL \texttt{div} operator is |
63167 | 110 |
mapped to the \<open>sdiv\<close> operator in Isabelle. The characteristic theorems |
111 |
of \<open>sdiv\<close>, in particular those describing the relationship with the standard |
|
112 |
\<open>div\<close> operator, are shown in \figref{fig:sdiv-properties} |
|
45044 | 113 |
\begin{figure} |
114 |
\begin{center} |
|
115 |
\small |
|
116 |
\begin{tabular}{ll} |
|
63167 | 117 |
\<open>sdiv_def\<close>: & @{thm sdiv_def} \\ |
118 |
\<open>sdiv_minus_dividend\<close>: & @{thm sdiv_minus_dividend} \\ |
|
119 |
\<open>sdiv_minus_divisor\<close>: & @{thm sdiv_minus_divisor} \\ |
|
120 |
\<open>sdiv_pos_pos\<close>: & @{thm [mode=no_brackets] sdiv_pos_pos} \\ |
|
121 |
\<open>sdiv_pos_neg\<close>: & @{thm [mode=no_brackets] sdiv_pos_neg} \\ |
|
122 |
\<open>sdiv_neg_pos\<close>: & @{thm [mode=no_brackets] sdiv_neg_pos} \\ |
|
123 |
\<open>sdiv_neg_neg\<close>: & @{thm [mode=no_brackets] sdiv_neg_neg} \\ |
|
45044 | 124 |
\end{tabular} |
125 |
\end{center} |
|
63167 | 126 |
\caption{Characteristic properties of \<open>sdiv\<close>} |
45044 | 127 |
\label{fig:sdiv-properties} |
128 |
\end{figure} |
|
129 |
||
130 |
\begin{figure} |
|
131 |
\begin{center} |
|
132 |
\small |
|
133 |
\begin{tabular}{ll} |
|
63167 | 134 |
\<open>AND_lower\<close>: & @{thm [mode=no_brackets] AND_lower} \\ |
135 |
\<open>OR_lower\<close>: & @{thm [mode=no_brackets] OR_lower} \\ |
|
136 |
\<open>XOR_lower\<close>: & @{thm [mode=no_brackets] XOR_lower} \\ |
|
137 |
\<open>AND_upper1\<close>: & @{thm [mode=no_brackets] AND_upper1} \\ |
|
138 |
\<open>AND_upper2\<close>: & @{thm [mode=no_brackets] AND_upper2} \\ |
|
139 |
\<open>OR_upper\<close>: & @{thm [mode=no_brackets] OR_upper} \\ |
|
140 |
\<open>XOR_upper\<close>: & @{thm [mode=no_brackets] XOR_upper} \\ |
|
141 |
\<open>AND_mod\<close>: & @{thm [mode=no_brackets] AND_mod} |
|
45044 | 142 |
\end{tabular} |
143 |
\end{center} |
|
144 |
\caption{Characteristic properties of bitwise operators} |
|
145 |
\label{fig:bitwise} |
|
146 |
\end{figure} |
|
147 |
The bitwise logical operators of \SPARK{} and FDL are modelled by the operators |
|
63167 | 148 |
\<open>AND\<close>, \<open>OR\<close> and \<open>XOR\<close> from Isabelle's \<open>Word\<close> library, |
45044 | 149 |
all of which have type @{typ "int \<Rightarrow> int \<Rightarrow> int"}. A list of properties of these |
150 |
operators that are useful in proofs about \SPARK{} programs are shown in |
|
151 |
\figref{fig:bitwise} |
|
63167 | 152 |
\<close> |
45044 | 153 |
|
63167 | 154 |
subsection \<open>Enumeration types\<close> |
45044 | 155 |
|
63167 | 156 |
text \<open> |
45044 | 157 |
The FDL enumeration type |
158 |
\begin{alltt} |
|
159 |
type \(t\) = (\(e\sb{1}\), \(e\sb{2}\), \dots, \(e\sb{n}\)); |
|
160 |
\end{alltt} |
|
161 |
is modelled by the Isabelle datatype |
|
162 |
\begin{isabelle} |
|
163 |
\normalsize |
|
164 |
\isacommand{datatype}\ $t$\ =\ $e_1$\ $\mid$\ $e_2$\ $\mid$\ \dots\ $\mid$\ $e_n$ |
|
165 |
\end{isabelle} |
|
166 |
The HOL-\SPARK{} environment defines a type class @{class spark_enum} that captures |
|
167 |
the characteristic properties of all enumeration types. It provides the following |
|
63167 | 168 |
polymorphic functions and constants for all types \<open>'a\<close> of this type class: |
45044 | 169 |
\begin{flushleft} |
170 |
@{term_type [mode=my_constrain] pos} \\ |
|
171 |
@{term_type [mode=my_constrain] val} \\ |
|
172 |
@{term_type [mode=my_constrain] succ} \\ |
|
173 |
@{term_type [mode=my_constrain] pred} \\ |
|
174 |
@{term_type [mode=my_constrain] first_el} \\ |
|
175 |
@{term_type [mode=my_constrain] last_el} |
|
176 |
\end{flushleft} |
|
177 |
In addition, @{class spark_enum} is a subclass of the @{class linorder} type class, |
|
63167 | 178 |
which allows the comparison operators \<open><\<close> and \<open>\<le>\<close> to be used on |
45044 | 179 |
enumeration types. The polymorphic operations shown above enjoy a number of |
180 |
generic properties that hold for all enumeration types. These properties are |
|
181 |
listed in \figref{fig:enum-generic-properties}. |
|
182 |
Moreover, \figref{fig:enum-specific-properties} shows a list of properties |
|
183 |
that are specific to each enumeration type $t$, such as the characteristic |
|
184 |
equations for @{term val} and @{term pos}. |
|
185 |
\begin{figure}[t] |
|
186 |
\begin{center} |
|
187 |
\small |
|
188 |
\begin{tabular}{ll} |
|
63167 | 189 |
\<open>range_pos\<close>: & @{thm range_pos} \\ |
190 |
\<open>less_pos\<close>: & @{thm less_pos} \\ |
|
191 |
\<open>less_eq_pos\<close>: & @{thm less_eq_pos} \\ |
|
192 |
\<open>val_def\<close>: & @{thm val_def} \\ |
|
193 |
\<open>succ_def\<close>: & @{thm succ_def} \\ |
|
194 |
\<open>pred_def\<close>: & @{thm pred_def} \\ |
|
195 |
\<open>first_el_def\<close>: & @{thm first_el_def} \\ |
|
196 |
\<open>last_el_def\<close>: & @{thm last_el_def} \\ |
|
197 |
\<open>inj_pos\<close>: & @{thm inj_pos} \\ |
|
198 |
\<open>val_pos\<close>: & @{thm val_pos} \\ |
|
199 |
\<open>pos_val\<close>: & @{thm pos_val} \\ |
|
200 |
\<open>first_el_smallest\<close>: & @{thm first_el_smallest} \\ |
|
201 |
\<open>last_el_greatest\<close>: & @{thm last_el_greatest} \\ |
|
202 |
\<open>pos_succ\<close>: & @{thm pos_succ} \\ |
|
203 |
\<open>pos_pred\<close>: & @{thm pos_pred} \\ |
|
204 |
\<open>succ_val\<close>: & @{thm succ_val} \\ |
|
205 |
\<open>pred_val\<close>: & @{thm pred_val} |
|
45044 | 206 |
\end{tabular} |
207 |
\end{center} |
|
208 |
\caption{Generic properties of functions on enumeration types} |
|
209 |
\label{fig:enum-generic-properties} |
|
210 |
\end{figure} |
|
211 |
\begin{figure}[t] |
|
212 |
\begin{center} |
|
213 |
\small |
|
214 |
\begin{tabular}{ll@ {\hspace{2cm}}ll} |
|
215 |
\texttt{$t$\_val}: & \isa{val\ $0$\ =\ $e_1$} & \texttt{$t$\_pos}: & pos\ $e_1$\ =\ $0$ \\ |
|
216 |
& \isa{val\ $1$\ =\ $e_2$} & & pos\ $e_2$\ =\ $1$ \\ |
|
217 |
& \hspace{1cm}\vdots & & \hspace{1cm}\vdots \\ |
|
218 |
& \isa{val\ $(n-1)$\ =\ $e_n$} & & pos\ $e_n$\ =\ $n-1$ |
|
219 |
\end{tabular} \\[3ex] |
|
220 |
\begin{tabular}{ll} |
|
221 |
\texttt{$t$\_card}: & \isa{card($t$)\ =\ $n$} \\ |
|
222 |
\texttt{$t$\_first\_el}: & \isa{first\_el\ =\ $e_1$} \\ |
|
223 |
\texttt{$t$\_last\_el}: & \isa{last\_el\ =\ $e_n$} |
|
224 |
\end{tabular} |
|
225 |
\end{center} |
|
226 |
\caption{Type-specific properties of functions on enumeration types} |
|
227 |
\label{fig:enum-specific-properties} |
|
228 |
\end{figure} |
|
63167 | 229 |
\<close> |
45044 | 230 |
|
63167 | 231 |
subsection \<open>Records\<close> |
45044 | 232 |
|
63167 | 233 |
text \<open> |
45044 | 234 |
The FDL record type |
235 |
\begin{alltt} |
|
236 |
type \(t\) = record |
|
237 |
\(f\sb{1}\) : \(t\sb{1}\); |
|
238 |
\(\vdots\) |
|
239 |
\(f\sb{n}\) : \(t\sb{n}\) |
|
240 |
end; |
|
241 |
\end{alltt} |
|
242 |
is modelled by the Isabelle record type |
|
243 |
\begin{isabelle} |
|
244 |
\normalsize |
|
245 |
\isacommand{record}\ t\ = \isanewline |
|
246 |
\ \ $f_1$\ ::\ $t_1$ \isanewline |
|
247 |
\ \ \ \vdots \isanewline |
|
248 |
\ \ $f_n$\ ::\ $t_n$ |
|
249 |
\end{isabelle} |
|
250 |
Records are constructed using the notation |
|
251 |
\isa{\isasymlparr$f_1$\ =\ $v_1$,\ $\ldots$,\ $f_n$\ =\ $v_n$\isasymrparr}, |
|
252 |
a field $f_i$ of a record $r$ is selected using the notation $f_i~r$, and the |
|
253 |
fields $f$ and $f'$ of a record $r$ can be updated using the notation |
|
254 |
\mbox{\isa{$r$\ \isasymlparr$f$\ :=\ $v$,\ $f'$\ :=\ $v'$\isasymrparr}}. |
|
63167 | 255 |
\<close> |
45044 | 256 |
|
63167 | 257 |
subsection \<open>Arrays\<close> |
45044 | 258 |
|
63167 | 259 |
text \<open> |
45044 | 260 |
The FDL array type |
261 |
\begin{alltt} |
|
262 |
type \(t\) = array [\(t\sb{1}\), \(\ldots\), \(t\sb{n}\)] of \(u\); |
|
263 |
\end{alltt} |
|
264 |
is modelled by the Isabelle function type $t_1 \times \cdots \times t_n \Rightarrow u$. |
|
265 |
Array updates are written as \isa{$A$($x_1$\ := $y_1$,\ \dots,\ $x_n$\ :=\ $y_n$)}. |
|
266 |
To allow updating an array at a set of indices, HOL-\SPARK{} provides the notation |
|
267 |
\isa{\dots\ [:=]\ \dots}, which can be combined with \isa{\dots\ :=\ \dots} and has |
|
268 |
the properties |
|
269 |
@{thm [display,mode=no_brackets] fun_upds_in fun_upds_notin upds_singleton} |
|
270 |
Thus, we can write expressions like |
|
271 |
@{term [display] "(A::int\<Rightarrow>int) ({0..9} [:=] 42, 15 := 99, {20..29} [:=] 0)"} |
|
272 |
that would be cumbersome to write using single updates. |
|
63167 | 273 |
\<close> |
45044 | 274 |
|
63167 | 275 |
section \<open>User-defined proof functions and types\<close> |
45044 | 276 |
|
63167 | 277 |
text \<open> |
45044 | 278 |
To illustrate the interplay between the commands for introducing user-defined proof |
279 |
functions and types mentioned in \secref{sec:spark-commands}, we now discuss a larger |
|
280 |
example involving the definition of proof functions on complex types. Assume we would |
|
281 |
like to define an array type, whose elements are records that themselves contain |
|
282 |
arrays. Moreover, assume we would like to initialize all array elements and record |
|
283 |
fields of type \texttt{Integer} in an array of this type with the value \texttt{0}. |
|
284 |
The specification of package \texttt{Complex\_Types} containing the definition of |
|
285 |
the array type, which we call \texttt{Array\_Type2}, is shown in \figref{fig:complex-types}. |
|
286 |
It also contains the declaration of a proof function \texttt{Initialized} that is used |
|
287 |
to express that the array has been initialized. The two other proof functions |
|
288 |
\texttt{Initialized2} and \texttt{Initialized3} are used to reason about the |
|
289 |
initialization of the inner array. Since the array types and proof functions |
|
290 |
may be used by several packages, such as the one shown in \figref{fig:complex-types-app}, |
|
291 |
it is advantageous to define the proof functions in a central theory that can |
|
292 |
be included by other theories containing proofs about packages using \texttt{Complex\_Types}. |
|
293 |
We show this theory in \figref{fig:complex-types-thy}. Since the proof functions |
|
294 |
refer to the enumeration and record types defined in \texttt{Complex\_Types}, |
|
295 |
we need to define the Isabelle counterparts of these types using the |
|
296 |
\isa{\isacommand{datatype}} and \isa{\isacommand{record}} commands in order |
|
297 |
to be able to write down the definition of the proof functions. These types are |
|
298 |
linked to the corresponding \SPARK{} types using the \isa{\isacommand{spark\_types}} |
|
299 |
command. Note that we have to specify the full name of the \SPARK{} functions |
|
300 |
including the package prefix. Using the logic of Isabelle, we can then define |
|
301 |
functions involving the enumeration and record types introduced above, and link |
|
302 |
them to the corresponding \SPARK{} proof functions. It is important that the |
|
303 |
\isa{\isacommand{definition}} commands are preceeded by the \isa{\isacommand{spark\_types}} |
|
63167 | 304 |
command, since the definition of \<open>initialized3\<close> uses the \<open>val\<close> |
305 |
function for enumeration types that is only available once that \<open>day\<close> |
|
45044 | 306 |
has been declared as a \SPARK{} type. |
307 |
\begin{figure} |
|
308 |
\lstinputlisting{complex_types.ads} |
|
309 |
\caption{Nested array and record types} |
|
310 |
\label{fig:complex-types} |
|
311 |
\end{figure} |
|
312 |
\begin{figure} |
|
313 |
\lstinputlisting{complex_types_app.ads} |
|
314 |
\lstinputlisting{complex_types_app.adb} |
|
315 |
\caption{Application of \texttt{Complex\_Types} package} |
|
316 |
\label{fig:complex-types-app} |
|
317 |
\end{figure} |
|
318 |
\begin{figure} |
|
319 |
\input{Complex_Types} |
|
320 |
\caption{Theory defining proof functions for complex types} |
|
321 |
\label{fig:complex-types-thy} |
|
322 |
\end{figure} |
|
63167 | 323 |
\<close> |
45044 | 324 |
|
325 |
(*<*) |
|
326 |
end |
|
327 |
(*>*) |