--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/document/intro.tex Thu Sep 22 16:50:23 2011 +0200
@@ -0,0 +1,129 @@
+\chapter{Introduction}
+\label{sec:intro}
+
+This document describes a link between Isabelle/HOL and the \SPARK{}/Ada tool
+suite for the verification of high-integrity software.
+Using this link, verification problems can be tackled that are beyond reach
+of the proof tools currently available for \SPARK{}. A number of examples
+can be found in the directory \texttt{HOL/SPARK/Examples} in the Isabelle
+distribution. An open-source version of the \SPARK{} tool suite is available
+free of charge from \hbox{\href{http://libre.adacore.com}{libre.adacore.com}}.
+
+In the remainder of \secref{sec:intro},
+we give an introduction to \SPARK{} and the HOL-\SPARK{} link. The verification
+of an example program is described in \secref{sec:example-verification}. In
+\secref{sec:vc-principles}, we explain the principles underlying the generation
+of verification conditions for \SPARK{} programs. Finally, \secref{sec:spark-reference}
+describes the commands provided by the HOL-\SPARK{} link, as well as the encoding
+of \SPARK{} types in HOL.
+
+\section{\SPARK{}}
+
+\SPARK{} \cite{Barnes} is a subset of the Ada language that has been designed to
+allow verification of high-integrity software. It is missing certain features of
+Ada that can make programs difficult to verify, such as \emph{access types},
+\emph{dynamic data structures}, and \emph{recursion}. \SPARK{} allows to prove
+absence of \emph{runtime exceptions}, as well as \emph{partial correctness}
+using pre- and postconditions. Loops can be annotated with \emph{invariants},
+and each procedure must have a \emph{dataflow annotation}, specifying the
+dependencies of the output parameters on the input parameters of the procedure.
+Since \SPARK{} annotations are just written as comments, \SPARK{} programs can be
+compiled by an ordinary Ada compiler such as GNAT. \SPARK{} comes with a number
+of tools, notably the \emph{Examiner} that, given a \SPARK{} program as an input,
+performs a \emph{dataflow analysis} and generates \emph{verification conditions}
+(VCs) that must be proved in order for the program to be exception-free and partially
+correct. The VCs generated by the Examiner are formulae expressed in
+a language called FDL, which is first-order logic extended with
+arithmetic operators, arrays, records, and enumeration types. For example,
+the FDL expression
+\begin{alltt}
+ for_all(i: integer, ((i >= min) and (i <= max)) ->
+ (element(a, [i]) = 0))
+\end{alltt}
+states that all elements of the array \texttt{a} with indices greater or equal to
+\texttt{min} and smaller or equal to \texttt{max} are $0$.
+VCs are processed by another \SPARK{} tool called the
+\emph{Simplifier} that either completely solves VCs or transforms them
+into simpler, equivalent conditions. The latter VCs
+can then be processed using another tool called
+the \emph{Proof Checker}. While the Simplifier tries to prove VCs in a completely
+automatic way, the Proof Checker requires user interaction, which enables it to
+prove formulae that are beyond the scope of the Simplifier. The steps
+that are required to manually prove a VC are recorded in a log file by the Proof
+Checker. Finally, this log file, together with the output of the other \SPARK{} tools
+mentioned above, is read by a tool called POGS (\textbf{P}roof \textbf{O}bli\textbf{G}ation
+\textbf{S}ummariser) that produces a table mentioning for each VC the method by which
+it has been proved.
+In order to overcome the limitations of FDL and to express complex specifications,
+\SPARK{} allows the user to declare so-called
+\emph{proof functions}. The desired properties of such functions are described
+by postulating a set of rules that can be used by the Simplifier and Proof Checker
+\cite[\S 11.7]{Barnes}. An obvious drawback of this approach is that incorrect
+rules can easily introduce inconsistencies.
+
+\section{HOL-\SPARK{}}
+
+The HOL-\SPARK{} verification environment, which is built on top of Isabelle's object
+logic HOL, is intended as an alternative
+to the \SPARK{} Proof Checker, and improves on it in a number of ways.
+HOL-\SPARK{} allows Isabelle to directly parse files generated
+by the Examiner and Simplifier, and provides a special proof command to conduct
+proofs of VCs, which can make use of the full power of Isabelle's rich
+collection of proof methods.
+Proofs can be conducted using Isabelle's graphical user interface, which makes
+it easy to navigate through larger proof scripts. Moreover, proof functions
+can be introduced in a \emph{definitional} way, for example by using Isabelle's
+package for recursive functions, rather than by just stating their properties as axioms,
+which avoids introducing inconsistencies.
+
+\begin{figure}
+\begin{center}
+\begin{tikzpicture}
+\tikzstyle{box}=[draw, drop shadow, fill=white, text width=3.5cm, text centered]
+\tikzstyle{rbox}=[draw, drop shadow, fill=white, rounded corners, minimum height=1cm]
+
+\node[box] (src) at (5,0) {Source files (\texttt{*.ads, *.adb})};
+\node[rbox] (exa) at (5,-2) {Examiner};
+\node[box] (fdl) at (0.5,-4) {FDL declarations \\ (\texttt{*.fdl})};
+\node[box] (vcs) at (5,-4) {VCs \\ (\texttt{*.vcg})};
+\node[box] (rls) at (9.5,-4) {Rules \\ (\texttt{*.rls})};
+\node[rbox] (simp) at (5,-6) {Simplifier};
+\node[box] (siv) at (5,-8) {Simplified VCs \\ (\texttt{*.siv})};
+\node[rbox] (isa) at (5,-10) {HOL-\SPARK{}};
+\node[box] (thy) at (9.5,-10) {Theory files \\ (\texttt{*.thy})};
+\node[box] (prv) at (5,-12) {Proof review files \\ (\texttt{*.prv})};
+\node[rbox] (pogs) at (5,-14) {POGS};
+\node[box] (sum) at (5,-16) {Summary file \\ (\texttt{*.sum})};
+
+\draw[-latex] (src) -- (exa);
+\draw[-latex] (exa) -- (fdl);
+\draw[-latex] (exa) -- (vcs);
+\draw[-latex] (exa) -- (rls);
+\draw[-latex] (fdl) -- (simp);
+\draw[-latex] (vcs) -- (simp);
+\draw[-latex] (rls) -- (simp);
+\draw[-latex] (simp) -- (siv);
+\draw[-latex] (fdl) .. controls (0.5,-8) .. (isa);
+\draw[-latex] (siv) -- (isa);
+\draw[-latex] (rls) .. controls (9.5,-8) .. (isa);
+\draw[-latex] (thy) -- (isa);
+\draw[-latex] (isa) -- (prv);
+\draw[-latex] (vcs) .. controls (-1,-6) and (-1,-13) .. (pogs);
+\draw[-latex] (siv) .. controls (1,-9) and (1,-12) .. (pogs);
+\draw[-latex] (prv) -- (pogs);
+\draw[-latex] (pogs) -- (sum);
+\end{tikzpicture}
+\end{center}
+\caption{\SPARK{} program verification tool chain}
+\label{fig:spark-toolchain}
+\end{figure}
+Figure \ref{fig:spark-toolchain} shows the integration of HOL-\SPARK{} into the
+tool chain for the verification of \SPARK{} programs. HOL-\SPARK{} processes declarations
+(\texttt{*.fdl}) and rules (\texttt{*.rls}) produced by the Examiner, as well as
+simplified VCs (\texttt{*.siv}) produced by the \SPARK{} Simplifier. Alternatively,
+the original unsimplified VCs (\texttt{*.vcg}) produced by the Examiner can be
+used as well. Processing of the \SPARK{} files is triggered by an Isabelle
+theory file (\texttt{*.thy}), which also contains the proofs for the VCs contained
+in the \texttt{*.siv} or \texttt{*.vcg} files. Once that all verification conditions
+have been successfully proved, Isabelle generates a proof review file (\texttt{*.prv})
+notifying the POGS tool of the VCs that have been discharged.