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