|
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. |