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