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