src/HOL/SPARK/Manual/Example_Verification.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (21 months ago)
changeset 67003 49850a679c2c
parent 66453 cc19f7ca2ed6
child 68407 fd61a2e4e1f9
permissions -rw-r--r--
more robust sorted_entries;
berghofe@45044
     1
(*<*)
berghofe@45044
     2
theory Example_Verification
wenzelm@66453
     3
imports "HOL-SPARK-Examples.Greatest_Common_Divisor" Simple_Greatest_Common_Divisor
berghofe@45044
     4
begin
berghofe@45044
     5
(*>*)
berghofe@45044
     6
wenzelm@63167
     7
chapter \<open>Verifying an Example Program\<close>
berghofe@45044
     8
wenzelm@63167
     9
text \<open>
berghofe@45044
    10
\label{sec:example-verification}
berghofe@45044
    11
\begin{figure}
berghofe@45044
    12
\lstinputlisting{Gcd.ads}
berghofe@45044
    13
\lstinputlisting{Gcd.adb}
berghofe@45044
    14
\caption{\SPARK{} program for computing the greatest common divisor}
berghofe@45044
    15
\label{fig:gcd-prog}
berghofe@45044
    16
\end{figure}
berghofe@45044
    17
berghofe@45044
    18
\begin{figure}
berghofe@45044
    19
\input{Greatest_Common_Divisor}
berghofe@45044
    20
\caption{Correctness proof for the greatest common divisor program}
berghofe@45044
    21
\label{fig:gcd-proof}
berghofe@45044
    22
\end{figure}
berghofe@45044
    23
We will now explain the usage of the \SPARK{} verification environment by proving
berghofe@45044
    24
the correctness of an example program. As an example, we use a program for computing
berghofe@45044
    25
the \emph{greatest common divisor} of two natural numbers shown in \figref{fig:gcd-prog},
wenzelm@58622
    26
which has been taken from the book about \SPARK{} by Barnes @{cite \<open>\S 11.6\<close> Barnes}.
wenzelm@63167
    27
\<close>
berghofe@45044
    28
wenzelm@63167
    29
section \<open>Importing \SPARK{} VCs into Isabelle\<close>
berghofe@45044
    30
wenzelm@63167
    31
text \<open>
berghofe@45044
    32
In order to specify that the \SPARK{} procedure \texttt{G\_C\_D} behaves like its
berghofe@45044
    33
mathematical counterpart, Barnes introduces a \emph{proof function} \texttt{Gcd}
berghofe@45044
    34
in the package specification. Invoking the \SPARK{} Examiner and Simplifier on
berghofe@45044
    35
this program yields a file \texttt{g\_c\_d.siv} containing the simplified VCs,
berghofe@45044
    36
as well as files \texttt{g\_c\_d.fdl} and \texttt{g\_c\_d.rls}, containing FDL
berghofe@45044
    37
declarations and rules, respectively. The files generated by \SPARK{} are assumed to reside in the
berghofe@45044
    38
subdirectory \texttt{greatest\_common\_divisor}. For \texttt{G\_C\_D} the
berghofe@45044
    39
Examiner generates ten VCs, eight of which are proved automatically by
berghofe@45044
    40
the Simplifier. We now show how to prove the remaining two VCs
berghofe@45044
    41
interactively using HOL-\SPARK{}. For this purpose, we create a \emph{theory}
berghofe@45044
    42
\texttt{Greatest\_Common\_Divisor}, which is shown in \figref{fig:gcd-proof}.
berghofe@45044
    43
A theory file always starts with the keyword \isa{\isacommand{theory}} followed
berghofe@45044
    44
by the name of the theory, which must be the same as the file name. The theory
berghofe@45044
    45
name is followed by the keyword \isa{\isacommand{imports}} and a list of theories
berghofe@45044
    46
imported by the current theory. All theories using the HOL-\SPARK{} verification
berghofe@45044
    47
environment must import the theory \texttt{SPARK}. In addition, we also include
berghofe@45044
    48
the \texttt{GCD} theory. The list of imported theories is followed by the
berghofe@45044
    49
\isa{\isacommand{begin}} keyword. In order to interactively process the theory
berghofe@45044
    50
shown in \figref{fig:gcd-proof}, we start Isabelle with the command
berghofe@45044
    51
\begin{verbatim}
berghofe@45044
    52
  isabelle emacs -l HOL-SPARK Greatest_Common_Divisor.thy
berghofe@45044
    53
\end{verbatim}
berghofe@45044
    54
The option ``\texttt{-l HOL-SPARK}'' instructs Isabelle to load the right
berghofe@45044
    55
object logic image containing the verification environment. Each proof function
berghofe@45044
    56
occurring in the specification of a \SPARK{} program must be linked with a
berghofe@45044
    57
corresponding Isabelle function. This is accomplished by the command
berghofe@45044
    58
\isa{\isacommand{spark\_proof\_functions}}, which expects a list of equations
berghofe@45044
    59
of the form \emph{name}\texttt{\ =\ }\emph{term}, where \emph{name} is the
berghofe@45044
    60
name of the proof function and \emph{term} is the corresponding Isabelle term.
berghofe@45044
    61
In the case of \texttt{gcd}, both the \SPARK{} proof function and its Isabelle
berghofe@45044
    62
counterpart happen to have the same name. Isabelle checks that the type of the
berghofe@45044
    63
term linked with a proof function agrees with the type of the function declared
berghofe@45044
    64
in the \texttt{*.fdl} file.
berghofe@45044
    65
It is worth noting that the
berghofe@45044
    66
\isa{\isacommand{spark\_proof\_functions}} command can be invoked both outside,
berghofe@45044
    67
i.e.\ before \isa{\isacommand{spark\_open}}, and inside the environment, i.e.\ after
berghofe@45044
    68
\isa{\isacommand{spark\_open}}, but before any \isa{\isacommand{spark\_vc}} command. The
berghofe@45044
    69
former variant is useful when having to declare proof functions that are shared by several
berghofe@45044
    70
procedures, whereas the latter has the advantage that the type of the proof function
berghofe@45044
    71
can be checked immediately, since the VCs, and hence also the declarations of proof
berghofe@45044
    72
functions in the \texttt{*.fdl} file have already been loaded.
berghofe@45044
    73
\begin{figure}
berghofe@45044
    74
\begin{flushleft}
berghofe@45044
    75
\tt
berghofe@45044
    76
Context: \\
berghofe@45044
    77
\ \\
berghofe@45044
    78
\begin{tabular}{ll}
wenzelm@63167
    79
fixes & \<open>m ::\<close>\ "\<open>int\<close>" \\
wenzelm@63167
    80
and   & \<open>n ::\<close>\ "\<open>int\<close>" \\
wenzelm@63167
    81
and   & \<open>c ::\<close>\ "\<open>int\<close>" \\
wenzelm@63167
    82
and   & \<open>d ::\<close>\ "\<open>int\<close>" \\
wenzelm@63167
    83
assumes & \<open>g_c_d_rules1:\<close>\ "\<open>0 \<le> integer__size\<close>" \\
wenzelm@63167
    84
and     & \<open>g_c_d_rules6:\<close>\ "\<open>0 \<le> natural__size\<close>" \\
berghofe@45044
    85
\multicolumn{2}{l}{notes definition} \\
wenzelm@63167
    86
\multicolumn{2}{l}{\hspace{2ex}\<open>defns =\<close>\ `\<open>integer__first = - 2147483648\<close>`} \\
wenzelm@63167
    87
\multicolumn{2}{l}{\hspace{4ex}`\<open>integer__last = 2147483647\<close>`} \\
berghofe@45044
    88
\multicolumn{2}{l}{\hspace{4ex}\dots}
berghofe@45044
    89
\end{tabular}\ \\[1.5ex]
berghofe@45044
    90
\ \\
berghofe@45044
    91
Definitions: \\
berghofe@45044
    92
\ \\
berghofe@45044
    93
\begin{tabular}{ll}
wenzelm@63167
    94
\<open>g_c_d_rules2:\<close> & \<open>integer__first = - 2147483648\<close> \\
wenzelm@63167
    95
\<open>g_c_d_rules3:\<close> & \<open>integer__last = 2147483647\<close> \\
berghofe@45044
    96
\dots
berghofe@45044
    97
\end{tabular}\ \\[1.5ex]
berghofe@45044
    98
\ \\
berghofe@45044
    99
Verification conditions: \\
berghofe@45044
   100
\ \\
berghofe@45044
   101
path(s) from assertion of line 10 to assertion of line 10 \\
berghofe@45044
   102
\ \\
wenzelm@63167
   103
\<open>procedure_g_c_d_4\<close>\ (unproved) \\
berghofe@45044
   104
\ \ \begin{tabular}{ll}
wenzelm@63167
   105
assumes & \<open>H1:\<close>\ "\<open>0 \<le> c\<close>" \\
wenzelm@63167
   106
and     & \<open>H2:\<close>\ "\<open>0 < d\<close>" \\
wenzelm@63167
   107
and     & \<open>H3:\<close>\ "\<open>gcd c d = gcd m n\<close>" \\
berghofe@45044
   108
\dots \\
wenzelm@63167
   109
shows & "\<open>0 < c - c sdiv d * d\<close>" \\
wenzelm@63167
   110
and   & "\<open>gcd d (c - c sdiv d * d) = gcd m n\<close>
berghofe@45044
   111
\end{tabular}\ \\[1.5ex]
berghofe@45044
   112
\ \\
berghofe@45044
   113
path(s) from assertion of line 10 to finish \\
berghofe@45044
   114
\ \\
wenzelm@63167
   115
\<open>procedure_g_c_d_11\<close>\ (unproved) \\
berghofe@45044
   116
\ \ \begin{tabular}{ll}
wenzelm@63167
   117
assumes & \<open>H1:\<close>\ "\<open>0 \<le> c\<close>" \\
wenzelm@63167
   118
and     & \<open>H2:\<close>\ "\<open>0 < d\<close>" \\
wenzelm@63167
   119
and     & \<open>H3:\<close>\ "\<open>gcd c d = gcd m n\<close>" \\
berghofe@45044
   120
\dots \\
wenzelm@63167
   121
shows & "\<open>d = gcd m n\<close>"
berghofe@45044
   122
\end{tabular}
berghofe@45044
   123
\end{flushleft}
berghofe@45044
   124
\caption{Output of \isa{\isacommand{spark\_status}} for \texttt{g\_c\_d.siv}}
berghofe@45044
   125
\label{fig:gcd-status}
berghofe@45044
   126
\end{figure}
berghofe@45044
   127
We now instruct Isabelle to open
berghofe@45044
   128
a new verification environment and load a set of VCs. This is done using the
berghofe@45044
   129
command \isa{\isacommand{spark\_open}}, which must be given the name of a
berghofe@56798
   130
\texttt{*.siv} file as an argument. Behind the scenes, Isabelle
berghofe@45044
   131
parses this file and the corresponding \texttt{*.fdl} and \texttt{*.rls} files,
berghofe@45044
   132
and converts the VCs to Isabelle terms. Using the command \isa{\isacommand{spark\_status}},
berghofe@45044
   133
the user can display the current VCs together with their status (proved, unproved).
berghofe@45044
   134
The variants \isa{\isacommand{spark\_status}\ (proved)}
berghofe@45044
   135
and \isa{\isacommand{spark\_status}\ (unproved)} show only proved and unproved
berghofe@45044
   136
VCs, respectively. For \texttt{g\_c\_d.siv}, the output of
berghofe@45044
   137
\isa{\isacommand{spark\_status}} is shown in \figref{fig:gcd-status}.
berghofe@45044
   138
To minimize the number of assumptions, and hence the size of the VCs,
berghofe@45044
   139
FDL rules of the form ``\dots\ \texttt{may\_be\_replaced\_by}\ \dots'' are
berghofe@45044
   140
turned into native Isabelle definitions, whereas other rules are modelled
berghofe@45044
   141
as assumptions.
wenzelm@63167
   142
\<close>
berghofe@45044
   143
wenzelm@63167
   144
section \<open>Proving the VCs\<close>
berghofe@45044
   145
wenzelm@63167
   146
text \<open>
berghofe@45044
   147
\label{sec:proving-vcs}
wenzelm@63167
   148
The two open VCs are \<open>procedure_g_c_d_4\<close> and \<open>procedure_g_c_d_11\<close>,
wenzelm@63167
   149
both of which contain the \<open>gcd\<close> proof function that the \SPARK{} Simplifier
berghofe@45044
   150
does not know anything about. The proof of a particular VC can be started with
berghofe@45044
   151
the \isa{\isacommand{spark\_vc}} command, which is similar to the standard
berghofe@45044
   152
\isa{\isacommand{lemma}} and \isa{\isacommand{theorem}} commands, with the
berghofe@45044
   153
difference that it only takes a name of a VC but no formula as an argument.
berghofe@45044
   154
A VC can have several conclusions that can be referenced by the identifiers
wenzelm@63167
   155
\<open>?C1\<close>, \<open>?C2\<close>, etc. If there is just one conclusion, it can
wenzelm@63167
   156
also be referenced by \<open>?thesis\<close>. It is important to note that the
wenzelm@63167
   157
\texttt{div} operator of FDL behaves differently from the \<open>div\<close> operator
berghofe@45044
   158
of Isabelle/HOL on negative numbers. The former always truncates towards zero,
berghofe@45044
   159
whereas the latter truncates towards minus infinity. This is why the FDL
wenzelm@63167
   160
\texttt{div} operator is mapped to the \<open>sdiv\<close> operator in Isabelle/HOL,
berghofe@45044
   161
which is defined as
berghofe@45044
   162
@{thm [display] sdiv_def}
berghofe@45044
   163
For example, we have that
berghofe@45044
   164
@{lemma "-5 sdiv 4 = -1" by (simp add: sdiv_neg_pos)}, but
berghofe@45044
   165
@{lemma "(-5::int) div 4 = -2" by simp}.
wenzelm@63167
   166
For non-negative dividend and divisor, \<open>sdiv\<close> is equivalent to \<open>div\<close>,
wenzelm@63167
   167
as witnessed by theorem \<open>sdiv_pos_pos\<close>:
berghofe@45044
   168
@{thm [display,mode=no_brackets] sdiv_pos_pos}
berghofe@45044
   169
In contrast, the behaviour of the FDL \texttt{mod} operator is equivalent to
berghofe@45044
   170
the one of Isabelle/HOL. Moreover, since FDL has no counterpart of the \SPARK{}
berghofe@45044
   171
operator \textbf{rem}, the \SPARK{} expression \texttt{c}\ \textbf{rem}\ \texttt{d}
wenzelm@63167
   172
just becomes \<open>c - c sdiv d * d\<close> in Isabelle. The first conclusion of
wenzelm@63167
   173
\<open>procedure_g_c_d_4\<close> requires us to prove that the remainder of \<open>c\<close>
wenzelm@63167
   174
and \<open>d\<close> is greater than \<open>0\<close>. To do this, we use the theorem
haftmann@64246
   175
\<open>minus_div_mult_eq_mod [symmetric]\<close> describing the correspondence between \<open>div\<close>
wenzelm@63167
   176
and \<open>mod\<close>
haftmann@64246
   177
@{thm [display] minus_div_mult_eq_mod [symmetric]}
wenzelm@63167
   178
together with the theorem \<open>pos_mod_sign\<close> saying that the result of the
wenzelm@63167
   179
\<open>mod\<close> operator is non-negative when applied to a non-negative divisor:
berghofe@45044
   180
@{thm [display] pos_mod_sign}
wenzelm@63167
   181
We will also need the aforementioned theorem \<open>sdiv_pos_pos\<close> in order for
wenzelm@63167
   182
the standard Isabelle/HOL theorems about \<open>div\<close> to be applicable
wenzelm@63167
   183
to the VC, which is formulated using \<open>sdiv\<close> rather that \<open>div\<close>.
wenzelm@63167
   184
Note that the proof uses \texttt{`\<open>0 \<le> c\<close>`} and \texttt{`\<open>0 < d\<close>`}
wenzelm@63167
   185
rather than \<open>H1\<close> and \<open>H2\<close> to refer to the hypotheses of the current
berghofe@45044
   186
VC. While the latter variant seems more compact, it is not particularly robust,
berghofe@45044
   187
since the numbering of hypotheses can easily change if the corresponding
berghofe@45044
   188
program is modified, making the proof script hard to adjust when there are many hypotheses.
wenzelm@63167
   189
Moreover, proof scripts using abbreviations like \<open>H1\<close> and \<open>H2\<close>
berghofe@45044
   190
are hard to read without assistance from Isabelle.
wenzelm@63167
   191
The second conclusion of \<open>procedure_g_c_d_4\<close> requires us to prove that
wenzelm@63167
   192
the \<open>gcd\<close> of \<open>d\<close> and the remainder of \<open>c\<close> and \<open>d\<close>
wenzelm@63167
   193
is equal to the \<open>gcd\<close> of the original input values \<open>m\<close> and \<open>n\<close>,
berghofe@45044
   194
which is the actual \emph{invariant} of the procedure. This is a consequence
wenzelm@63167
   195
of theorem \<open>gcd_non_0_int\<close>
berghofe@45044
   196
@{thm [display] gcd_non_0_int}
haftmann@64246
   197
Again, we also need theorems \<open>minus_div_mult_eq_mod [symmetric]\<close> and \<open>sdiv_pos_pos\<close>
berghofe@45044
   198
to justify that \SPARK{}'s \textbf{rem} operator is equivalent to Isabelle's
wenzelm@63167
   199
\<open>mod\<close> operator for non-negative operands.
wenzelm@63167
   200
The VC \<open>procedure_g_c_d_11\<close> says that if the loop invariant holds before
berghofe@45044
   201
the last iteration of the loop, the postcondition of the procedure will hold
berghofe@45044
   202
after execution of the loop body. To prove this, we observe that the remainder
wenzelm@63167
   203
of \<open>c\<close> and \<open>d\<close>, and hence \<open>c mod d\<close> is \<open>0\<close> when exiting
wenzelm@63167
   204
the loop. This implies that \<open>gcd c d = d\<close>, since \<open>c\<close> is divisible
wenzelm@63167
   205
by \<open>d\<close>, so the conclusion follows using the assumption \<open>gcd c d = gcd m n\<close>.
berghofe@45044
   206
This concludes the proofs of the open VCs, and hence the \SPARK{} verification
berghofe@45044
   207
environment can be closed using the command \isa{\isacommand{spark\_end}}.
berghofe@45044
   208
This command checks that all VCs have been proved and issues an error message
berghofe@45044
   209
if there are remaining unproved VCs. Moreover, Isabelle checks that there is
berghofe@45044
   210
no open \SPARK{} verification environment when the final \isa{\isacommand{end}}
berghofe@45044
   211
command of a theory is encountered.
wenzelm@63167
   212
\<close>
berghofe@45044
   213
wenzelm@63167
   214
section \<open>Optimizing the proof\<close>
berghofe@45044
   215
wenzelm@63167
   216
text \<open>
berghofe@45044
   217
\begin{figure}
berghofe@45044
   218
\lstinputlisting{Simple_Gcd.adb}
berghofe@45044
   219
\input{Simple_Greatest_Common_Divisor}
berghofe@45044
   220
\caption{Simplified greatest common divisor program and proof}
berghofe@45044
   221
\label{fig:simple-gcd-proof}
berghofe@45044
   222
\end{figure}
berghofe@45044
   223
When looking at the program from \figref{fig:gcd-prog} once again, several
berghofe@45044
   224
optimizations come to mind. First of all, like the input parameters of the
berghofe@45044
   225
procedure, the local variables \texttt{C}, \texttt{D}, and \texttt{R} can
berghofe@45044
   226
be declared as \texttt{Natural} rather than \texttt{Integer}. Since natural
berghofe@45044
   227
numbers are non-negative by construction, the values computed by the algorithm
berghofe@45044
   228
are trivially proved to be non-negative. Since we are working with non-negative
berghofe@45044
   229
numbers, we can also just use \SPARK{}'s \textbf{mod} operator instead of
haftmann@64246
   230
\textbf{rem}, which spares us an application of theorems \<open>minus_div_mult_eq_mod [symmetric]\<close>
wenzelm@63167
   231
and \<open>sdiv_pos_pos\<close>. Finally, as noted by Barnes @{cite \<open>\S 11.5\<close> Barnes},
berghofe@45044
   232
we can simplify matters by placing the \textbf{assert} statement between
berghofe@45044
   233
\textbf{while} and \textbf{loop} rather than directly after the \textbf{loop}.
berghofe@45044
   234
In the former case, the loop invariant has to be proved only once, whereas in
berghofe@45044
   235
the latter case, it has to be proved twice: since the \textbf{assert} occurs after
berghofe@45044
   236
the check of the exit condition, the invariant has to be proved for the path
berghofe@45044
   237
from the \textbf{assert} statement to the \textbf{assert} statement, and for
berghofe@45044
   238
the path from the \textbf{assert} statement to the postcondition. In the case
berghofe@45044
   239
of the \texttt{G\_C\_D} procedure, this might not seem particularly problematic,
berghofe@45044
   240
since the proof of the invariant is very simple, but it can unnecessarily
berghofe@45044
   241
complicate matters if the proof of the invariant is non-trivial. The simplified
berghofe@45044
   242
program for computing the greatest common divisor, together with its correctness
berghofe@45044
   243
proof, is shown in \figref{fig:simple-gcd-proof}. Since the package specification
berghofe@45044
   244
has not changed, we only show the body of the packages. The two VCs can now be
wenzelm@63167
   245
proved by a single application of Isabelle's proof method \<open>simp\<close>.
wenzelm@63167
   246
\<close>
berghofe@45044
   247
berghofe@45044
   248
(*<*)
berghofe@45044
   249
end
berghofe@45044
   250
(*>*)