45044
|
1 |
\chapter{Introduction}
|
|
2 |
\label{sec:intro}
|
|
3 |
|
|
4 |
This document describes a link between Isabelle/HOL and the \SPARK{}/Ada tool
|
|
5 |
suite for the verification of high-integrity software.
|
|
6 |
Using this link, verification problems can be tackled that are beyond reach
|
|
7 |
of the proof tools currently available for \SPARK{}. A number of examples
|
|
8 |
can be found in the directory \texttt{HOL/SPARK/Examples} in the Isabelle
|
|
9 |
distribution. An open-source version of the \SPARK{} tool suite is available
|
|
10 |
free of charge from \hbox{\href{http://libre.adacore.com}{libre.adacore.com}}.
|
|
11 |
|
|
12 |
In the remainder of \secref{sec:intro},
|
|
13 |
we give an introduction to \SPARK{} and the HOL-\SPARK{} link. The verification
|
|
14 |
of an example program is described in \secref{sec:example-verification}. In
|
|
15 |
\secref{sec:vc-principles}, we explain the principles underlying the generation
|
|
16 |
of verification conditions for \SPARK{} programs. Finally, \secref{sec:spark-reference}
|
|
17 |
describes the commands provided by the HOL-\SPARK{} link, as well as the encoding
|
|
18 |
of \SPARK{} types in HOL.
|
|
19 |
|
|
20 |
\section{\SPARK{}}
|
|
21 |
|
|
22 |
\SPARK{} \cite{Barnes} is a subset of the Ada language that has been designed to
|
|
23 |
allow verification of high-integrity software. It is missing certain features of
|
|
24 |
Ada that can make programs difficult to verify, such as \emph{access types},
|
|
25 |
\emph{dynamic data structures}, and \emph{recursion}. \SPARK{} allows to prove
|
|
26 |
absence of \emph{runtime exceptions}, as well as \emph{partial correctness}
|
|
27 |
using pre- and postconditions. Loops can be annotated with \emph{invariants},
|
|
28 |
and each procedure must have a \emph{dataflow annotation}, specifying the
|
|
29 |
dependencies of the output parameters on the input parameters of the procedure.
|
|
30 |
Since \SPARK{} annotations are just written as comments, \SPARK{} programs can be
|
|
31 |
compiled by an ordinary Ada compiler such as GNAT. \SPARK{} comes with a number
|
|
32 |
of tools, notably the \emph{Examiner} that, given a \SPARK{} program as an input,
|
|
33 |
performs a \emph{dataflow analysis} and generates \emph{verification conditions}
|
|
34 |
(VCs) that must be proved in order for the program to be exception-free and partially
|
|
35 |
correct. The VCs generated by the Examiner are formulae expressed in
|
|
36 |
a language called FDL, which is first-order logic extended with
|
|
37 |
arithmetic operators, arrays, records, and enumeration types. For example,
|
|
38 |
the FDL expression
|
|
39 |
\begin{alltt}
|
|
40 |
for_all(i: integer, ((i >= min) and (i <= max)) ->
|
|
41 |
(element(a, [i]) = 0))
|
|
42 |
\end{alltt}
|
|
43 |
states that all elements of the array \texttt{a} with indices greater or equal to
|
|
44 |
\texttt{min} and smaller or equal to \texttt{max} are $0$.
|
|
45 |
VCs are processed by another \SPARK{} tool called the
|
|
46 |
\emph{Simplifier} that either completely solves VCs or transforms them
|
|
47 |
into simpler, equivalent conditions. The latter VCs
|
|
48 |
can then be processed using another tool called
|
|
49 |
the \emph{Proof Checker}. While the Simplifier tries to prove VCs in a completely
|
|
50 |
automatic way, the Proof Checker requires user interaction, which enables it to
|
|
51 |
prove formulae that are beyond the scope of the Simplifier. The steps
|
|
52 |
that are required to manually prove a VC are recorded in a log file by the Proof
|
|
53 |
Checker. Finally, this log file, together with the output of the other \SPARK{} tools
|
|
54 |
mentioned above, is read by a tool called POGS (\textbf{P}roof \textbf{O}bli\textbf{G}ation
|
|
55 |
\textbf{S}ummariser) that produces a table mentioning for each VC the method by which
|
|
56 |
it has been proved.
|
|
57 |
In order to overcome the limitations of FDL and to express complex specifications,
|
|
58 |
\SPARK{} allows the user to declare so-called
|
|
59 |
\emph{proof functions}. The desired properties of such functions are described
|
|
60 |
by postulating a set of rules that can be used by the Simplifier and Proof Checker
|
|
61 |
\cite[\S 11.7]{Barnes}. An obvious drawback of this approach is that incorrect
|
|
62 |
rules can easily introduce inconsistencies.
|
|
63 |
|
|
64 |
\section{HOL-\SPARK{}}
|
|
65 |
|
|
66 |
The HOL-\SPARK{} verification environment, which is built on top of Isabelle's object
|
|
67 |
logic HOL, is intended as an alternative
|
|
68 |
to the \SPARK{} Proof Checker, and improves on it in a number of ways.
|
|
69 |
HOL-\SPARK{} allows Isabelle to directly parse files generated
|
|
70 |
by the Examiner and Simplifier, and provides a special proof command to conduct
|
|
71 |
proofs of VCs, which can make use of the full power of Isabelle's rich
|
|
72 |
collection of proof methods.
|
|
73 |
Proofs can be conducted using Isabelle's graphical user interface, which makes
|
|
74 |
it easy to navigate through larger proof scripts. Moreover, proof functions
|
|
75 |
can be introduced in a \emph{definitional} way, for example by using Isabelle's
|
|
76 |
package for recursive functions, rather than by just stating their properties as axioms,
|
|
77 |
which avoids introducing inconsistencies.
|
|
78 |
|
|
79 |
\begin{figure}
|
|
80 |
\begin{center}
|
|
81 |
\begin{tikzpicture}
|
|
82 |
\tikzstyle{box}=[draw, drop shadow, fill=white, text width=3.5cm, text centered]
|
|
83 |
\tikzstyle{rbox}=[draw, drop shadow, fill=white, rounded corners, minimum height=1cm]
|
|
84 |
|
|
85 |
\node[box] (src) at (5,0) {Source files (\texttt{*.ads, *.adb})};
|
|
86 |
\node[rbox] (exa) at (5,-2) {Examiner};
|
|
87 |
\node[box] (fdl) at (0.5,-4) {FDL declarations \\ (\texttt{*.fdl})};
|
|
88 |
\node[box] (vcs) at (5,-4) {VCs \\ (\texttt{*.vcg})};
|
|
89 |
\node[box] (rls) at (9.5,-4) {Rules \\ (\texttt{*.rls})};
|
|
90 |
\node[rbox] (simp) at (5,-6) {Simplifier};
|
|
91 |
\node[box] (siv) at (5,-8) {Simplified VCs \\ (\texttt{*.siv})};
|
|
92 |
\node[rbox] (isa) at (5,-10) {HOL-\SPARK{}};
|
|
93 |
\node[box] (thy) at (9.5,-10) {Theory files \\ (\texttt{*.thy})};
|
|
94 |
\node[box] (prv) at (5,-12) {Proof review files \\ (\texttt{*.prv})};
|
|
95 |
\node[rbox] (pogs) at (5,-14) {POGS};
|
|
96 |
\node[box] (sum) at (5,-16) {Summary file \\ (\texttt{*.sum})};
|
|
97 |
|
|
98 |
\draw[-latex] (src) -- (exa);
|
|
99 |
\draw[-latex] (exa) -- (fdl);
|
|
100 |
\draw[-latex] (exa) -- (vcs);
|
|
101 |
\draw[-latex] (exa) -- (rls);
|
|
102 |
\draw[-latex] (fdl) -- (simp);
|
|
103 |
\draw[-latex] (vcs) -- (simp);
|
|
104 |
\draw[-latex] (rls) -- (simp);
|
|
105 |
\draw[-latex] (simp) -- (siv);
|
|
106 |
\draw[-latex] (fdl) .. controls (0.5,-8) .. (isa);
|
|
107 |
\draw[-latex] (siv) -- (isa);
|
|
108 |
\draw[-latex] (rls) .. controls (9.5,-8) .. (isa);
|
|
109 |
\draw[-latex] (thy) -- (isa);
|
|
110 |
\draw[-latex] (isa) -- (prv);
|
|
111 |
\draw[-latex] (vcs) .. controls (-1,-6) and (-1,-13) .. (pogs);
|
|
112 |
\draw[-latex] (siv) .. controls (1,-9) and (1,-12) .. (pogs);
|
|
113 |
\draw[-latex] (prv) -- (pogs);
|
|
114 |
\draw[-latex] (pogs) -- (sum);
|
|
115 |
\end{tikzpicture}
|
|
116 |
\end{center}
|
|
117 |
\caption{\SPARK{} program verification tool chain}
|
|
118 |
\label{fig:spark-toolchain}
|
|
119 |
\end{figure}
|
|
120 |
Figure \ref{fig:spark-toolchain} shows the integration of HOL-\SPARK{} into the
|
|
121 |
tool chain for the verification of \SPARK{} programs. HOL-\SPARK{} processes declarations
|
|
122 |
(\texttt{*.fdl}) and rules (\texttt{*.rls}) produced by the Examiner, as well as
|
|
123 |
simplified VCs (\texttt{*.siv}) produced by the \SPARK{} Simplifier. Alternatively,
|
|
124 |
the original unsimplified VCs (\texttt{*.vcg}) produced by the Examiner can be
|
|
125 |
used as well. Processing of the \SPARK{} files is triggered by an Isabelle
|
|
126 |
theory file (\texttt{*.thy}), which also contains the proofs for the VCs contained
|
|
127 |
in the \texttt{*.siv} or \texttt{*.vcg} files. Once that all verification conditions
|
|
128 |
have been successfully proved, Isabelle generates a proof review file (\texttt{*.prv})
|
|
129 |
notifying the POGS tool of the VCs that have been discharged.
|