author  wenzelm 
Mon, 06 Apr 2015 17:28:07 +0200  
changeset 59938  f84b93187ab6 
parent 58130  5e9170812356 
child 61143  5f898411ce87 
permissions  rwrr 
45044  1 
(*<*) 
2 
theory Reference 

58130  3 
imports "../SPARK" 
45044  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:sparkreference} 

14 
This section is intended as a quick reference for the HOL\SPARK{} verification 

15 
environment. In \secref{sec:sparkcommands}, we give a summary of the commands 

16 
provided by the HOL\SPARK{}, while \secref{sec:sparktypes} 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:sparkcommands} 

24 
This section describes the syntax and effect of each of the commands provided 

25 
by HOL\SPARK{}. 

59938  26 
@{rail \<open> 
27 
@'spark_open' name ('(' name ')')? 

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  32 
files must reside in the same directory as the file given as an argument to the command. 
33 
This command also generates records and datatypes for the types specified in the 

34 
\texttt{*.fdl} file, unless they have already been associated with userdefined 

35 
Isabelle types (see below). 

36 
Since 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 

38 
format \texttt{$p_1$\_\_$\ldots$\_\_$p_n$}. When working with projects consisting of several 

39 
packages, this is necessary in order for the verification environment to be able to map proof 

40 
functions and types defined in Isabelle to their \SPARK{} counterparts. 

59938  41 
@{rail \<open> 
42 
@'spark_proof_functions' ((name '=' term)+) 

43 
\<close>} 

45044  44 
Associates a proof function with the given name to a term. The name should be the full name 
45 
of the proof function as it appears in the \texttt{*.fdl} file, including the package prefix. 

46 
This command can be used both inside and outside a verification environment. The latter 

47 
variant is useful for introducing proof functions that are shared by several procedures 

48 
or packages, whereas the former allows the given term to refer to the types generated 

49 
by \isa{\isacommand{spark\_open}} for record or enumeration types specified in the 

50 
\texttt{*.fdl} file. 

59938  51 
@{rail \<open> 
52 
@'spark_types' ((name '=' type (mapping?))+) 

53 
; 

54 
mapping: '('((name '=' nameref)+',')')' 

55 
\<close>} 

45044  56 
Associates a \SPARK{} type with the given name with an Isabelle type. This command can 
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  62 
proof functions referring to record or enumeration types that are shared by several 
63 
procedures or packages. First, the types required by the proof functions can be introduced 

64 
using Isabelle's commands for defining records or datatypes. Having introduced the 

65 
types, the proof functions can be defined in Isabelle. Finally, both the proof 

66 
functions and the types can be associated with their \SPARK{} counterparts. 

59938  67 
@{rail \<open> 
68 
@'spark_status' (('(proved)'  '(unproved)')?) 

69 
\<close>} 

45044  70 
Outputs the variables declared in the \texttt{*.fdl} file, the rules declared in 
71 
the \texttt{*.rls} file, and all VCs, together with their status (proved, unproved). 

72 
The output can be restricted to the proved or unproved VCs by giving the corresponding 

73 
option to the command. 

59938  74 
@{rail \<open> 
75 
@'spark_vc' name 

76 
\<close>} 

45044  77 
Initiates the proof of the VC with the given name. Similar to the standard 
78 
\isa{\isacommand{lemma}} or \isa{\isacommand{theorem}} commands, this command 

79 
must be followed by a sequence of proof commands. The command introduces the 

80 
hypotheses \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. 

59938  82 
@{rail \<open> 
83 
@'spark_end' '(incomplete)'? 

84 
\<close>} 

48168  85 
Closes the current verification environment. Unless the \texttt{incomplete} 
86 
option is given, all VCs must have been proved, 

45044  87 
otherwise the command issues an error message. As a side effect, the command 
88 
generates a proof review (\texttt{*.prv}) file to inform POGS of the proved 

89 
VCs. 

90 
*} 

91 

92 
section {* Types *} 

93 

94 
text {* 

95 
\label{sec:sparktypes} 

96 
The main types of FDL are integers, enumeration types, records, and arrays. 

97 
In the following sections, we describe how these types are modelled in 

98 
Isabelle. 

99 
*} 

100 

101 
subsection {* Integers *} 

102 

103 
text {* 

104 
The FDL type \texttt{integer} is modelled by the Isabelle type @{typ int}. 

105 
While the FDL \texttt{mod} operator behaves in the same way as its Isabelle 

106 
counterpart, this is not the case for the \texttt{div} operator. As has already 

107 
been mentioned in \secref{sec:provingvcs}, the \texttt{div} operator of \SPARK{} 

108 
always truncates towards zero, whereas the @{text div} operator of Isabelle 

109 
truncates towards minus infinity. Therefore, the FDL \texttt{div} operator is 

110 
mapped to the @{text sdiv} operator in Isabelle. The characteristic theorems 

111 
of @{text sdiv}, in particular those describing the relationship with the standard 

112 
@{text div} operator, are shown in \figref{fig:sdivproperties} 

113 
\begin{figure} 

114 
\begin{center} 

115 
\small 

116 
\begin{tabular}{ll} 

117 
@{text sdiv_def}: & @{thm sdiv_def} \\ 

118 
@{text sdiv_minus_dividend}: & @{thm sdiv_minus_dividend} \\ 

119 
@{text sdiv_minus_divisor}: & @{thm sdiv_minus_divisor} \\ 

120 
@{text sdiv_pos_pos}: & @{thm [mode=no_brackets] sdiv_pos_pos} \\ 

121 
@{text sdiv_pos_neg}: & @{thm [mode=no_brackets] sdiv_pos_neg} \\ 

122 
@{text sdiv_neg_pos}: & @{thm [mode=no_brackets] sdiv_neg_pos} \\ 

123 
@{text sdiv_neg_neg}: & @{thm [mode=no_brackets] sdiv_neg_neg} \\ 

124 
\end{tabular} 

125 
\end{center} 

126 
\caption{Characteristic properties of @{text sdiv}} 

127 
\label{fig:sdivproperties} 

128 
\end{figure} 

129 

130 
\begin{figure} 

131 
\begin{center} 

132 
\small 

133 
\begin{tabular}{ll} 

134 
@{text AND_lower}: & @{thm [mode=no_brackets] AND_lower} \\ 

135 
@{text OR_lower}: & @{thm [mode=no_brackets] OR_lower} \\ 

136 
@{text XOR_lower}: & @{thm [mode=no_brackets] XOR_lower} \\ 

137 
@{text AND_upper1}: & @{thm [mode=no_brackets] AND_upper1} \\ 

138 
@{text AND_upper2}: & @{thm [mode=no_brackets] AND_upper2} \\ 

139 
@{text OR_upper}: & @{thm [mode=no_brackets] OR_upper} \\ 

140 
@{text XOR_upper}: & @{thm [mode=no_brackets] XOR_upper} \\ 

141 
@{text AND_mod}: & @{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} 

147 
The bitwise logical operators of \SPARK{} and FDL are modelled by the operators 

148 
@{text AND}, @{text OR} and @{text XOR} from Isabelle's @{text Word} library, 

149 
all of which have type @{typ "int \<Rightarrow> int \<Rightarrow> int"}. A list of properties of these 

150 
operators that are useful in proofs about \SPARK{} programs are shown in 

151 
\figref{fig:bitwise} 

152 
*} 

153 

154 
subsection {* Enumeration types *} 

155 

156 
text {* 

157 
The FDL enumeration type 

158 
\begin{alltt} 

159 
type \(t\) = (\(e\sb{1}\), \(e\sb{2}\), \dots, \(e\sb{n}\)); 

160 
\end{alltt} 

161 
is 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} 

166 
The HOL\SPARK{} environment defines a type class @{class spark_enum} that captures 

167 
the characteristic properties of all enumeration types. It provides the following 

168 
polymorphic functions and constants for all types @{text "'a"} 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} 

177 
In addition, @{class spark_enum} is a subclass of the @{class linorder} type class, 

178 
which allows the comparison operators @{text "<"} and @{text "\<le>"} to be used on 

179 
enumeration types. The polymorphic operations shown above enjoy a number of 

180 
generic properties that hold for all enumeration types. These properties are 

181 
listed in \figref{fig:enumgenericproperties}. 

182 
Moreover, \figref{fig:enumspecificproperties} shows a list of properties 

183 
that are specific to each enumeration type $t$, such as the characteristic 

184 
equations for @{term val} and @{term pos}. 

185 
\begin{figure}[t] 

186 
\begin{center} 

187 
\small 

188 
\begin{tabular}{ll} 

189 
@{text range_pos}: & @{thm range_pos} \\ 

190 
@{text less_pos}: & @{thm less_pos} \\ 

191 
@{text less_eq_pos}: & @{thm less_eq_pos} \\ 

192 
@{text val_def}: & @{thm val_def} \\ 

193 
@{text succ_def}: & @{thm succ_def} \\ 

194 
@{text pred_def}: & @{thm pred_def} \\ 

195 
@{text first_el_def}: & @{thm first_el_def} \\ 

196 
@{text last_el_def}: & @{thm last_el_def} \\ 

197 
@{text inj_pos}: & @{thm inj_pos} \\ 

198 
@{text val_pos}: & @{thm val_pos} \\ 

199 
@{text pos_val}: & @{thm pos_val} \\ 

200 
@{text first_el_smallest}: & @{thm first_el_smallest} \\ 

201 
@{text last_el_greatest}: & @{thm last_el_greatest} \\ 

202 
@{text pos_succ}: & @{thm pos_succ} \\ 

203 
@{text pos_pred}: & @{thm pos_pred} \\ 

204 
@{text succ_val}: & @{thm succ_val} \\ 

205 
@{text pred_val}: & @{thm pred_val} 

206 
\end{tabular} 

207 
\end{center} 

208 
\caption{Generic properties of functions on enumeration types} 

209 
\label{fig:enumgenericproperties} 

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\ $(n1)$\ =\ $e_n$} & & pos\ $e_n$\ =\ $n1$ 

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{Typespecific properties of functions on enumeration types} 

227 
\label{fig:enumspecificproperties} 

228 
\end{figure} 

229 
*} 

230 

231 
subsection {* Records *} 

232 

233 
text {* 

234 
The FDL record type 

235 
\begin{alltt} 

236 
type \(t\) = record 

237 
\(f\sb{1}\) : \(t\sb{1}\); 

238 
\(\vdots\) 

239 
\(f\sb{n}\) : \(t\sb{n}\) 

240 
end; 

241 
\end{alltt} 

242 
is 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} 

250 
Records are constructed using the notation 

251 
\isa{\isasymlparr$f_1$\ =\ $v_1$,\ $\ldots$,\ $f_n$\ =\ $v_n$\isasymrparr}, 

252 
a field $f_i$ of a record $r$ is selected using the notation $f_i~r$, and the 

253 
fields $f$ and $f'$ of a record $r$ can be updated using the notation 

254 
\mbox{\isa{$r$\ \isasymlparr$f$\ :=\ $v$,\ $f'$\ :=\ $v'$\isasymrparr}}. 

255 
*} 

256 

257 
subsection {* Arrays *} 

258 

259 
text {* 

260 
The FDL array type 

261 
\begin{alltt} 

262 
type \(t\) = array [\(t\sb{1}\), \(\ldots\), \(t\sb{n}\)] of \(u\); 

263 
\end{alltt} 

264 
is modelled by the Isabelle function type $t_1 \times \cdots \times t_n \Rightarrow u$. 

265 
Array updates are written as \isa{$A$($x_1$\ := $y_1$,\ \dots,\ $x_n$\ :=\ $y_n$)}. 

266 
To 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 

268 
the properties 

269 
@{thm [display,mode=no_brackets] fun_upds_in fun_upds_notin upds_singleton} 

270 
Thus, we can write expressions like 

271 
@{term [display] "(A::int\<Rightarrow>int) ({0..9} [:=] 42, 15 := 99, {20..29} [:=] 0)"} 

272 
that would be cumbersome to write using single updates. 

273 
*} 

274 

275 
section {* Userdefined proof functions and types *} 

276 

277 
text {* 

278 
To illustrate the interplay between the commands for introducing userdefined proof 

279 
functions and types mentioned in \secref{sec:sparkcommands}, we now discuss a larger 

280 
example involving the definition of proof functions on complex types. Assume we would 

281 
like to define an array type, whose elements are records that themselves contain 

282 
arrays. Moreover, assume we would like to initialize all array elements and record 

283 
fields of type \texttt{Integer} in an array of this type with the value \texttt{0}. 

284 
The specification of package \texttt{Complex\_Types} containing the definition of 

285 
the array type, which we call \texttt{Array\_Type2}, is shown in \figref{fig:complextypes}. 

286 
It also contains the declaration of a proof function \texttt{Initialized} that is used 

287 
to express that the array has been initialized. The two other proof functions 

288 
\texttt{Initialized2} and \texttt{Initialized3} are used to reason about the 

289 
initialization of the inner array. Since the array types and proof functions 

290 
may be used by several packages, such as the one shown in \figref{fig:complextypesapp}, 

291 
it is advantageous to define the proof functions in a central theory that can 

292 
be included by other theories containing proofs about packages using \texttt{Complex\_Types}. 

293 
We show this theory in \figref{fig:complextypesthy}. Since the proof functions 

294 
refer to the enumeration and record types defined in \texttt{Complex\_Types}, 

295 
we need to define the Isabelle counterparts of these types using the 

296 
\isa{\isacommand{datatype}} and \isa{\isacommand{record}} commands in order 

297 
to be able to write down the definition of the proof functions. These types are 

298 
linked to the corresponding \SPARK{} types using the \isa{\isacommand{spark\_types}} 

299 
command. Note that we have to specify the full name of the \SPARK{} functions 

300 
including the package prefix. Using the logic of Isabelle, we can then define 

301 
functions involving the enumeration and record types introduced above, and link 

302 
them to the corresponding \SPARK{} proof functions. It is important that the 

303 
\isa{\isacommand{definition}} commands are preceeded by the \isa{\isacommand{spark\_types}} 

304 
command, since the definition of @{text initialized3} uses the @{text val} 

305 
function for enumeration types that is only available once that @{text day} 

306 
has been declared as a \SPARK{} type. 

307 
\begin{figure} 

308 
\lstinputlisting{complex_types.ads} 

309 
\caption{Nested array and record types} 

310 
\label{fig:complextypes} 

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:complextypesapp} 

317 
\end{figure} 

318 
\begin{figure} 

319 
\input{Complex_Types} 

320 
\caption{Theory defining proof functions for complex types} 

321 
\label{fig:complextypesthy} 

322 
\end{figure} 

323 
*} 

324 

325 
(*<*) 

326 
end 

327 
(*>*) 