src/HOL/SPARK/Manual/Reference.thy
 author berghofe Thu Sep 22 16:50:23 2011 +0200 (2011-09-22) changeset 45044 2fae15f8984d child 46725 d34ec0512dfb permissions -rw-r--r--
     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 (*>*)