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