Quelle Example_Verification.thy

Sprache: Isabelle

(*<*)
theory Example_Verification
imports "HOL-SPARK-Examples.Greatest_Common_Divisor" Simple_Greatest_Common_Divisor
begin
(*>*)

chapter ‹Verifying an Example Program›

text ‹
label{sec:example-verification}
begin{figure}
lstinputlisting{Gcd.ads}
lstinputlisting{Gcd.adb}
caption{\SPARK{} program for computing the greatest common divisor}
label{fig:gcd-prog}
end{figure}

begin{figure}
input{Greatest_Common_Divisor}
caption{Correctness proof for the greatest common divisor program}
label{fig:gcd-proof}
end{figure}
will now explain the usage of the \SPARK{} verification environment by proving
correctness of an example program. As an example, we use a program for computing
\emph{greatest common divisor} of two natural numbers shown in \figref{fig:gcd-prog},
has been taken from the book about \SPARK{} by Barnes cite‹‹\S 11.6› in Barnes›.
›

section ‹Importing \SPARK{} VCs into Isabelle›

text ‹
order to specify that the \SPARK{} procedure \texttt{G\_C\_D} behaves like its
counterpart, Barnes introduces a \emph{proof function} \texttt{Gcd}
the package specification. Invoking the \SPARK{} Examiner and Simplifier on
program yields a file \texttt{g\_c\_d.siv} containing the simplified VCs,
well as files \texttt{g\_c\_d.fdl} and \texttt{g\_c\_d.rls}, containing FDL
and rules, respectively. The files generated by \SPARK{} are assumed to reside in the
\texttt{greatest\_common\_divisor}. For \texttt{G\_C\_D} the
generates ten VCs, eight of which are proved automatically by
Simplifier. We now show how to prove the remaining two VCs
using HOL-\SPARK{}. For this purpose, we create a \emph{theory}
texttt{Greatest\_Common\_Divisor}, which is shown in \figref{fig:gcd-proof}.
theory file always starts with the keyword \isa{\isacommand{theory}} followed
the name of the theory, which must be the same as the file name. The theory
is followed by the keyword \isa{\isacommand{imports}} and a list of theories
by the current theory. All theories using the HOL-\SPARK{} verification
must import the theory \texttt{SPARK}. In addition, we also include
\texttt{GCD} theory. The list of imported theories is followed by the
isa{\isacommand{begin}} keyword. In order to interactively process the theory
in \figref{fig:gcd-proof}, we start Isabelle with the command
begin{verbatim}
isabelle jedit -l HOL-SPARK Greatest_Common_Divisor.thy
end{verbatim}
option ``\texttt{-l HOL-SPARK}'' instructs Isabelle to load the right
logic image containing the verification environment. Each proof function
in the specification of a \SPARK{} program must be linked with a
Isabelle function. This is accomplished by the command
isa{\isacommand{spark\_proof\_functions}}, which expects a list of equations
the form \emph{name}\texttt{\ =\ }\emph{term}, where \emph{name} is the
of the proof function and \emph{term} is the corresponding Isabelle term.
the case of \texttt{gcd}, both the \SPARK{} proof function and its Isabelle
happen to have the same name. Isabelle checks that the type of the
linked with a proof function agrees with the type of the function declared
the \texttt{*.fdl} file.
is worth noting that the
isa{\isacommand{spark\_proof\_functions}} command can be invoked both outside,
.e.\ before \isa{\isacommand{spark\_open}}, and inside the environment, i.e.\ after
isa{\isacommand{spark\_open}}, but before any \isa{\isacommand{spark\_vc}} command. The
variant is useful when having to declare proof functions that are shared by several
, whereas the latter has the advantage that the type of the proof function
be checked immediately, since the VCs, and hence also the declarations of proof
in the \texttt{*.fdl} file have already been loaded.
begin{figure}
begin{flushleft}
tt
: \\
\\
begin{tabular}{ll}
& ‹m ::›\ "‹int›" \\
& ‹n ::›\ "‹int›" \\
& ‹c ::›\ "‹int›" \\
& ‹d ::›\ "‹int›" \\
& ‹g_c_d_rules1:›\ "‹0 ≤ integer__size›" \\
& ‹g_c_d_rules6:›\ "‹0 ≤ natural__size›" \\
multicolumn{2}{l}{notes definition} \\
multicolumn{2}{l}{\hspace{2ex}‹defns =›\ `‹integer__first = - 2147483648›`} \\
multicolumn{2}{l}{\hspace{4ex}`‹integer__last = 2147483647›`} \\
multicolumn{2}{l}{\hspace{4ex}\dots}
end{tabular}\ \\[1.5ex]
\\
: \\
\\
begin{tabular}{ll}
‹g_c_d_rules2:› & ‹integer__first = - 2147483648› \\
‹g_c_d_rules3:› & ‹integer__last = 2147483647› \\
dots
end{tabular}\ \\[1.5ex]
\\
conditions: \\
\\
(s) from assertion of line 10 to assertion of line 10 \\
\\
‹procedure_g_c_d_4›\ (unproved) \\
\ \begin{tabular}{ll}
& ‹H1:›\ "‹0 ≤ c›" \\
& ‹H2:›\ "‹0 < d›" \\
& ‹H3:›\ "‹gcd c d = gcd m n›" \\
dots \\
& "‹0 < c - c sdiv d * d›" \\
& "‹gcd d (c - c sdiv d * d) = gcd m n›
end{tabular}\ \\[1.5ex]
\\
(s) from assertion of line 10 to finish \\
\\
‹procedure_g_c_d_11›\ (unproved) \\
\ \begin{tabular}{ll}
& ‹H1:›\ "‹0 ≤ c›" \\
& ‹H2:›\ "‹0 < d›" \\
& ‹H3:›\ "‹gcd c d = gcd m n›" \\
dots \\
& "‹d = gcd m n›"
end{tabular}
end{flushleft}
caption{Output of \isa{\isacommand{spark\_status}} for \texttt{g\_c\_d.siv}}
label{fig:gcd-status}
end{figure}
now instruct Isabelle to open
new verification environment and load a set of VCs. This is done using the
\isa{\isacommand{spark\_open}}, which must be given the name of a
texttt{*.siv} file as an argument. Behind the scenes, Isabelle
this file and the corresponding \texttt{*.fdl} and \texttt{*.rls} files,
converts the VCs to Isabelle terms. Using the command \isa{\isacommand{spark\_status}},
user can display the current VCs together with their status (proved, unproved).
variants \isa{\isacommand{spark\_status}\ (proved)}
\isa{\isacommand{spark\_status}\ (unproved)} show only proved and unproved
, respectively. For \texttt{g\_c\_d.siv}, the output of
isa{\isacommand{spark\_status}} is shown in \figref{fig:gcd-status}.
minimize the number of assumptions, and hence the size of the VCs,
rules of the form ``\dots\ \texttt{may\_be\_replaced\_by}\ \dots'' are
into native Isabelle definitions, whereas other rules are modelled
assumptions.
›

section ‹Proving the VCs›

text ‹
label{sec:proving-vcs}
two open VCs are ‹procedure_g_c_d_4› and ‹procedure_g_c_d_11›,
of which contain the ‹gcd› proof function that the \SPARK{} Simplifier
not know anything about. The proof of a particular VC can be started with
\isa{\isacommand{spark\_vc}} command, which is similar to the standard
isa{\isacommand{lemma}} and \isa{\isacommand{theorem}} commands, with the
that it only takes a name of a VC but no formula as an argument.
VC can have several conclusions that can be referenced by the identifiers
‹?C1›, ‹?C2›, etc. If there is just one conclusion, it can
be referenced by ‹?thesis›. It is important to note that the
texttt{div} operator of FDL behaves differently from the ‹div› operator
Isabelle/HOL on negative numbers. The former always truncates towards zero,
the latter truncates towards minus infinity. This is why the FDL
texttt{div} operator is mapped to the ‹sdiv› operator in Isabelle/HOL,
is defined as
{thm [display] sdiv_def}
example, we have that
{lemma "-5 sdiv 4 = -1" by (simp add: sdiv_neg_pos)}, but
{lemma "(-5::int) div 4 = -2" by simp}.
non-negative dividend and divisor, ‹sdiv› is equivalent to ‹div›,
witnessed by theorem ‹sdiv_pos_pos›:
{thm [display,mode=no_brackets] sdiv_pos_pos}
contrast, the behaviour of the FDL \texttt{mod} operator is equivalent to
one of Isabelle/HOL. Moreover, since FDL has no counterpart of the \SPARK{}
\textbf{rem}, the \SPARK{} expression \texttt{c}\ \textbf{rem}\ \texttt{d}
becomes ‹c - c sdiv d * d› in Isabelle. The first conclusion of
‹procedure_g_c_d_4› requires us to prove that the remainder of ‹c›
‹d› is greater than ‹0›. To do this, we use the theorem
‹minus_div_mult_eq_mod [symmetric]› describing the correspondence between ‹div›
‹mod›
{thm [display] minus_div_mult_eq_mod [symmetric]}
with the theorem ‹pos_mod_sign› saying that the result of the
‹mod› operator is non-negative when applied to a non-negative divisor:
{thm [display] pos_mod_sign}
will also need the aforementioned theorem ‹sdiv_pos_pos› in order for
standard Isabelle/HOL theorems about ‹div› to be applicable
the VC, which is formulated using ‹sdiv› rather that ‹div›.
that the proof uses \texttt{`‹0 ≤ c›`} and \texttt{`‹0 < d›`}
than ‹H1› and ‹H2› to refer to the hypotheses of the current
. While the latter variant seems more compact, it is not particularly robust,
the numbering of hypotheses can easily change if the corresponding
is modified, making the proof script hard to adjust when there are many hypotheses.
, proof scripts using abbreviations like ‹H1› and ‹H2›
hard to read without assistance from Isabelle.
second conclusion of ‹procedure_g_c_d_4› requires us to prove that
‹gcd› of ‹d› and the remainder of ‹c› and ‹d›
equal to the ‹gcd› of the original input values ‹m› and ‹n›,
is the actual \emph{invariant} of the procedure. This is a consequence
theorem ‹gcd_non_0_int›
{thm [display] gcd_non_0_int}
, we also need theorems ‹minus_div_mult_eq_mod [symmetric]› and ‹sdiv_pos_pos›
justify that \SPARK{}'s \textbf{rem} operator is equivalent to Isabelle's
‹mod› operator for non-negative operands.
VC ‹procedure_g_c_d_11› says that if the loop invariant holds before
last iteration of the loop, the postcondition of the procedure will hold
execution of the loop body. To prove this, we observe that the remainder
‹c› and ‹d›, and hence ‹c mod d› is ‹0› when exiting
loop. This implies that ‹gcd c d = d›, since ‹c› is divisible
‹d›, so the conclusion follows using the assumption ‹gcd c d = gcd m n›.
concludes the proofs of the open VCs, and hence the \SPARK{} verification
can be closed using the command \isa{\isacommand{spark\_end}}.
command checks that all VCs have been proved and issues an error message
there are remaining unproved VCs. Moreover, Isabelle checks that there is
open \SPARK{} verification environment when the final \isa{\isacommand{end}}
of a theory is encountered.
›

section ‹Optimizing the proof›

text ‹
begin{figure}
lstinputlisting{Simple_Gcd.adb}
input{Simple_Greatest_Common_Divisor}
caption{Simplified greatest common divisor program and proof}
label{fig:simple-gcd-proof}
end{figure}
looking at the program from \figref{fig:gcd-prog} once again, several
come to mind. First of all, like the input parameters of the
, the local variables \texttt{C}, \texttt{D}, and \texttt{R} can
declared as \texttt{Natural} rather than \texttt{Integer}. Since natural
are non-negative by construction, the values computed by the algorithm
trivially proved to be non-negative. Since we are working with non-negative
, we can also just use \SPARK{}'s \textbf{mod} operator instead of
textbf{rem}, which spares us an application of theorems ‹minus_div_mult_eq_mod [symmetric]›
‹sdiv_pos_pos›. Finally, as noted by Barnes cite‹‹\S 11.5› in Barnes›,
can simplify matters by placing the \textbf{assert} statement between
textbf{while} and \textbf{loop} rather than directly after the \textbf{loop}.
the former case, the loop invariant has to be proved only once, whereas in
latter case, it has to be proved twice: since the \textbf{assert} occurs after
check of the exit condition, the invariant has to be proved for the path
the \textbf{assert} statement to the \textbf{assert} statement, and for
path from the \textbf{assert} statement to the postcondition. In the case
the \texttt{G\_C\_D} procedure, this might not seem particularly problematic,
the proof of the invariant is very simple, but it can unnecessarily
matters if the proof of the invariant is non-trivial. The simplified
for computing the greatest common divisor, together with its correctness
, is shown in \figref{fig:simple-gcd-proof}. Since the package specification
not changed, we only show the body of the packages. The two VCs can now be
by a single application of Isabelle's proof method ‹simp›.
›

(*<*)
end
(*>*)

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet am 2026-06-30) ¤

Wurzel

Suchen

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.