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