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