berghofe@45044: (*<*)
berghofe@45044: theory Example_Verification
berghofe@45044: imports "../Examples/Gcd/Greatest_Common_Divisor" Simple_Greatest_Common_Divisor
berghofe@45044: begin
berghofe@45044: (*>*)
berghofe@45044:
berghofe@45044: chapter {* Verifying an Example Program *}
berghofe@45044:
berghofe@45044: text {*
berghofe@45044: \label{sec:example-verification}
berghofe@45044: \begin{figure}
berghofe@45044: \lstinputlisting{Gcd.ads}
berghofe@45044: \lstinputlisting{Gcd.adb}
berghofe@45044: \caption{\SPARK{} program for computing the greatest common divisor}
berghofe@45044: \label{fig:gcd-prog}
berghofe@45044: \end{figure}
berghofe@45044:
berghofe@45044: \begin{figure}
berghofe@45044: \input{Greatest_Common_Divisor}
berghofe@45044: \caption{Correctness proof for the greatest common divisor program}
berghofe@45044: \label{fig:gcd-proof}
berghofe@45044: \end{figure}
berghofe@45044: We will now explain the usage of the \SPARK{} verification environment by proving
berghofe@45044: the correctness of an example program. As an example, we use a program for computing
berghofe@45044: the \emph{greatest common divisor} of two natural numbers shown in \figref{fig:gcd-prog},
berghofe@45044: which has been taken from the book about \SPARK{} by Barnes \cite[\S 11.6]{Barnes}.
berghofe@45044: *}
berghofe@45044:
berghofe@45044: section {* Importing \SPARK{} VCs into Isabelle *}
berghofe@45044:
berghofe@45044: text {*
berghofe@45044: In order to specify that the \SPARK{} procedure \texttt{G\_C\_D} behaves like its
berghofe@45044: mathematical counterpart, Barnes introduces a \emph{proof function} \texttt{Gcd}
berghofe@45044: in the package specification. Invoking the \SPARK{} Examiner and Simplifier on
berghofe@45044: this program yields a file \texttt{g\_c\_d.siv} containing the simplified VCs,
berghofe@45044: as well as files \texttt{g\_c\_d.fdl} and \texttt{g\_c\_d.rls}, containing FDL
berghofe@45044: declarations and rules, respectively. The files generated by \SPARK{} are assumed to reside in the
berghofe@45044: subdirectory \texttt{greatest\_common\_divisor}. For \texttt{G\_C\_D} the
berghofe@45044: Examiner generates ten VCs, eight of which are proved automatically by
berghofe@45044: the Simplifier. We now show how to prove the remaining two VCs
berghofe@45044: interactively using HOL-\SPARK{}. For this purpose, we create a \emph{theory}
berghofe@45044: \texttt{Greatest\_Common\_Divisor}, which is shown in \figref{fig:gcd-proof}.
berghofe@45044: A theory file always starts with the keyword \isa{\isacommand{theory}} followed
berghofe@45044: by the name of the theory, which must be the same as the file name. The theory
berghofe@45044: name is followed by the keyword \isa{\isacommand{imports}} and a list of theories
berghofe@45044: imported by the current theory. All theories using the HOL-\SPARK{} verification
berghofe@45044: environment must import the theory \texttt{SPARK}. In addition, we also include
berghofe@45044: the \texttt{GCD} theory. The list of imported theories is followed by the
berghofe@45044: \isa{\isacommand{begin}} keyword. In order to interactively process the theory
berghofe@45044: shown in \figref{fig:gcd-proof}, we start Isabelle with the command
berghofe@45044: \begin{verbatim}
berghofe@45044: isabelle emacs -l HOL-SPARK Greatest_Common_Divisor.thy
berghofe@45044: \end{verbatim}
berghofe@45044: The option ``\texttt{-l HOL-SPARK}'' instructs Isabelle to load the right
berghofe@45044: object logic image containing the verification environment. Each proof function
berghofe@45044: occurring in the specification of a \SPARK{} program must be linked with a
berghofe@45044: corresponding Isabelle function. This is accomplished by the command
berghofe@45044: \isa{\isacommand{spark\_proof\_functions}}, which expects a list of equations
berghofe@45044: of the form \emph{name}\texttt{\ =\ }\emph{term}, where \emph{name} is the
berghofe@45044: name of the proof function and \emph{term} is the corresponding Isabelle term.
berghofe@45044: In the case of \texttt{gcd}, both the \SPARK{} proof function and its Isabelle
berghofe@45044: counterpart happen to have the same name. Isabelle checks that the type of the
berghofe@45044: term linked with a proof function agrees with the type of the function declared
berghofe@45044: in the \texttt{*.fdl} file.
berghofe@45044: It is worth noting that the
berghofe@45044: \isa{\isacommand{spark\_proof\_functions}} command can be invoked both outside,
berghofe@45044: i.e.\ before \isa{\isacommand{spark\_open}}, and inside the environment, i.e.\ after
berghofe@45044: \isa{\isacommand{spark\_open}}, but before any \isa{\isacommand{spark\_vc}} command. The
berghofe@45044: former variant is useful when having to declare proof functions that are shared by several
berghofe@45044: procedures, whereas the latter has the advantage that the type of the proof function
berghofe@45044: can be checked immediately, since the VCs, and hence also the declarations of proof
berghofe@45044: functions in the \texttt{*.fdl} file have already been loaded.
berghofe@45044: \begin{figure}
berghofe@45044: \begin{flushleft}
berghofe@45044: \tt
berghofe@45044: Context: \\
berghofe@45044: \ \\
berghofe@45044: \begin{tabular}{ll}
berghofe@45044: fixes & @{text "m ::"}\ "@{text int}" \\
berghofe@45044: and & @{text "n ::"}\ "@{text int}" \\
berghofe@45044: and & @{text "c ::"}\ "@{text int}" \\
berghofe@45044: and & @{text "d ::"}\ "@{text int}" \\
berghofe@45044: assumes & @{text "g_c_d_rules1:"}\ "@{text "0 \ integer__size"}" \\
berghofe@45044: and & @{text "g_c_d_rules6:"}\ "@{text "0 \ natural__size"}" \\
berghofe@45044: \multicolumn{2}{l}{notes definition} \\
berghofe@45044: \multicolumn{2}{l}{\hspace{2ex}@{text "defns ="}\ `@{text "integer__first = - 2147483648"}`} \\
berghofe@45044: \multicolumn{2}{l}{\hspace{4ex}`@{text "integer__last = 2147483647"}`} \\
berghofe@45044: \multicolumn{2}{l}{\hspace{4ex}\dots}
berghofe@45044: \end{tabular}\ \\[1.5ex]
berghofe@45044: \ \\
berghofe@45044: Definitions: \\
berghofe@45044: \ \\
berghofe@45044: \begin{tabular}{ll}
berghofe@45044: @{text "g_c_d_rules2:"} & @{text "integer__first = - 2147483648"} \\
berghofe@45044: @{text "g_c_d_rules3:"} & @{text "integer__last = 2147483647"} \\
berghofe@45044: \dots
berghofe@45044: \end{tabular}\ \\[1.5ex]
berghofe@45044: \ \\
berghofe@45044: Verification conditions: \\
berghofe@45044: \ \\
berghofe@45044: path(s) from assertion of line 10 to assertion of line 10 \\
berghofe@45044: \ \\
berghofe@45044: @{text procedure_g_c_d_4}\ (unproved) \\
berghofe@45044: \ \ \begin{tabular}{ll}
berghofe@45044: assumes & @{text "H1:"}\ "@{text "0 \ c"}" \\
berghofe@45044: and & @{text "H2:"}\ "@{text "0 < d"}" \\
berghofe@45044: and & @{text "H3:"}\ "@{text "gcd c d = gcd m n"}" \\
berghofe@45044: \dots \\
berghofe@45044: shows & "@{text "0 < c - c sdiv d * d"}" \\
berghofe@45044: and & "@{text "gcd d (c - c sdiv d * d) = gcd m n"}
berghofe@45044: \end{tabular}\ \\[1.5ex]
berghofe@45044: \ \\
berghofe@45044: path(s) from assertion of line 10 to finish \\
berghofe@45044: \ \\
berghofe@45044: @{text procedure_g_c_d_11}\ (unproved) \\
berghofe@45044: \ \ \begin{tabular}{ll}
berghofe@45044: assumes & @{text "H1:"}\ "@{text "0 \ c"}" \\
berghofe@45044: and & @{text "H2:"}\ "@{text "0 < d"}" \\
berghofe@45044: and & @{text "H3:"}\ "@{text "gcd c d = gcd m n"}" \\
berghofe@45044: \dots \\
berghofe@45044: shows & "@{text "d = gcd m n"}"
berghofe@45044: \end{tabular}
berghofe@45044: \end{flushleft}
berghofe@45044: \caption{Output of \isa{\isacommand{spark\_status}} for \texttt{g\_c\_d.siv}}
berghofe@45044: \label{fig:gcd-status}
berghofe@45044: \end{figure}
berghofe@45044: We now instruct Isabelle to open
berghofe@45044: a new verification environment and load a set of VCs. This is done using the
berghofe@45044: command \isa{\isacommand{spark\_open}}, which must be given the name of a
berghofe@45044: \texttt{*.siv} or \texttt{*.vcg} file as an argument. Behind the scenes, Isabelle
berghofe@45044: parses this file and the corresponding \texttt{*.fdl} and \texttt{*.rls} files,
berghofe@45044: and converts the VCs to Isabelle terms. Using the command \isa{\isacommand{spark\_status}},
berghofe@45044: the user can display the current VCs together with their status (proved, unproved).
berghofe@45044: The variants \isa{\isacommand{spark\_status}\ (proved)}
berghofe@45044: and \isa{\isacommand{spark\_status}\ (unproved)} show only proved and unproved
berghofe@45044: VCs, respectively. For \texttt{g\_c\_d.siv}, the output of
berghofe@45044: \isa{\isacommand{spark\_status}} is shown in \figref{fig:gcd-status}.
berghofe@45044: To minimize the number of assumptions, and hence the size of the VCs,
berghofe@45044: FDL rules of the form ``\dots\ \texttt{may\_be\_replaced\_by}\ \dots'' are
berghofe@45044: turned into native Isabelle definitions, whereas other rules are modelled
berghofe@45044: as assumptions.
berghofe@45044: *}
berghofe@45044:
berghofe@45044: section {* Proving the VCs *}
berghofe@45044:
berghofe@45044: text {*
berghofe@45044: \label{sec:proving-vcs}
berghofe@45044: The two open VCs are @{text procedure_g_c_d_4} and @{text procedure_g_c_d_11},
berghofe@45044: both of which contain the @{text gcd} proof function that the \SPARK{} Simplifier
berghofe@45044: does not know anything about. The proof of a particular VC can be started with
berghofe@45044: the \isa{\isacommand{spark\_vc}} command, which is similar to the standard
berghofe@45044: \isa{\isacommand{lemma}} and \isa{\isacommand{theorem}} commands, with the
berghofe@45044: difference that it only takes a name of a VC but no formula as an argument.
berghofe@45044: A VC can have several conclusions that can be referenced by the identifiers
berghofe@45044: @{text "?C1"}, @{text "?C2"}, etc. If there is just one conclusion, it can
berghofe@45044: also be referenced by @{text "?thesis"}. It is important to note that the
berghofe@45044: \texttt{div} operator of FDL behaves differently from the @{text div} operator
berghofe@45044: of Isabelle/HOL on negative numbers. The former always truncates towards zero,
berghofe@45044: whereas the latter truncates towards minus infinity. This is why the FDL
berghofe@45044: \texttt{div} operator is mapped to the @{text sdiv} operator in Isabelle/HOL,
berghofe@45044: which is defined as
berghofe@45044: @{thm [display] sdiv_def}
berghofe@45044: For example, we have that
berghofe@45044: @{lemma "-5 sdiv 4 = -1" by (simp add: sdiv_neg_pos)}, but
berghofe@45044: @{lemma "(-5::int) div 4 = -2" by simp}.
berghofe@45044: For non-negative dividend and divisor, @{text sdiv} is equivalent to @{text div},
berghofe@45044: as witnessed by theorem @{text sdiv_pos_pos}:
berghofe@45044: @{thm [display,mode=no_brackets] sdiv_pos_pos}
berghofe@45044: In contrast, the behaviour of the FDL \texttt{mod} operator is equivalent to
berghofe@45044: the one of Isabelle/HOL. Moreover, since FDL has no counterpart of the \SPARK{}
berghofe@45044: operator \textbf{rem}, the \SPARK{} expression \texttt{c}\ \textbf{rem}\ \texttt{d}
berghofe@45044: just becomes @{text "c - c sdiv d * d"} in Isabelle. The first conclusion of
berghofe@45044: @{text procedure_g_c_d_4} requires us to prove that the remainder of @{text c}
berghofe@45044: and @{text d} is greater than @{text 0}. To do this, we use the theorem
berghofe@45044: @{text zmod_zdiv_equality'} describing the correspondence between @{text div}
berghofe@45044: and @{text mod}
berghofe@45044: @{thm [display] zmod_zdiv_equality'}
berghofe@45044: together with the theorem @{text pos_mod_sign} saying that the result of the
berghofe@45044: @{text mod} operator is non-negative when applied to a non-negative divisor:
berghofe@45044: @{thm [display] pos_mod_sign}
berghofe@45044: We will also need the aforementioned theorem @{text sdiv_pos_pos} in order for
berghofe@45044: the standard Isabelle/HOL theorems about @{text div} to be applicable
berghofe@45044: to the VC, which is formulated using @{text sdiv} rather that @{text div}.
berghofe@45044: Note that the proof uses \texttt{`@{text "0 \ c"}`} and \texttt{`@{text "0 < d"}`}
berghofe@45044: rather than @{text H1} and @{text H2} to refer to the hypotheses of the current
berghofe@45044: VC. While the latter variant seems more compact, it is not particularly robust,
berghofe@45044: since the numbering of hypotheses can easily change if the corresponding
berghofe@45044: program is modified, making the proof script hard to adjust when there are many hypotheses.
berghofe@45044: Moreover, proof scripts using abbreviations like @{text H1} and @{text H2}
berghofe@45044: are hard to read without assistance from Isabelle.
berghofe@45044: The second conclusion of @{text procedure_g_c_d_4} requires us to prove that
berghofe@45044: the @{text gcd} of @{text d} and the remainder of @{text c} and @{text d}
berghofe@45044: is equal to the @{text gcd} of the original input values @{text m} and @{text n},
berghofe@45044: which is the actual \emph{invariant} of the procedure. This is a consequence
berghofe@45044: of theorem @{text gcd_non_0_int}
berghofe@45044: @{thm [display] gcd_non_0_int}
berghofe@45044: Again, we also need theorems @{text zmod_zdiv_equality'} and @{text sdiv_pos_pos}
berghofe@45044: to justify that \SPARK{}'s \textbf{rem} operator is equivalent to Isabelle's
berghofe@45044: @{text mod} operator for non-negative operands.
berghofe@45044: The VC @{text procedure_g_c_d_11} says that if the loop invariant holds before
berghofe@45044: the last iteration of the loop, the postcondition of the procedure will hold
berghofe@45044: after execution of the loop body. To prove this, we observe that the remainder
berghofe@45044: of @{text c} and @{text d}, and hence @{text "c mod d"} is @{text 0} when exiting
berghofe@45044: the loop. This implies that @{text "gcd c d = d"}, since @{text c} is divisible
berghofe@45044: by @{text d}, so the conclusion follows using the assumption @{text "gcd c d = gcd m n"}.
berghofe@45044: This concludes the proofs of the open VCs, and hence the \SPARK{} verification
berghofe@45044: environment can be closed using the command \isa{\isacommand{spark\_end}}.
berghofe@45044: This command checks that all VCs have been proved and issues an error message
berghofe@45044: if there are remaining unproved VCs. Moreover, Isabelle checks that there is
berghofe@45044: no open \SPARK{} verification environment when the final \isa{\isacommand{end}}
berghofe@45044: command of a theory is encountered.
berghofe@45044: *}
berghofe@45044:
berghofe@45044: section {* Optimizing the proof *}
berghofe@45044:
berghofe@45044: text {*
berghofe@45044: \begin{figure}
berghofe@45044: \lstinputlisting{Simple_Gcd.adb}
berghofe@45044: \input{Simple_Greatest_Common_Divisor}
berghofe@45044: \caption{Simplified greatest common divisor program and proof}
berghofe@45044: \label{fig:simple-gcd-proof}
berghofe@45044: \end{figure}
berghofe@45044: When looking at the program from \figref{fig:gcd-prog} once again, several
berghofe@45044: optimizations come to mind. First of all, like the input parameters of the
berghofe@45044: procedure, the local variables \texttt{C}, \texttt{D}, and \texttt{R} can
berghofe@45044: be declared as \texttt{Natural} rather than \texttt{Integer}. Since natural
berghofe@45044: numbers are non-negative by construction, the values computed by the algorithm
berghofe@45044: are trivially proved to be non-negative. Since we are working with non-negative
berghofe@45044: numbers, we can also just use \SPARK{}'s \textbf{mod} operator instead of
berghofe@45044: \textbf{rem}, which spares us an application of theorems @{text zmod_zdiv_equality'}
berghofe@45044: and @{text sdiv_pos_pos}. Finally, as noted by Barnes \cite[\S 11.5]{Barnes},
berghofe@45044: we can simplify matters by placing the \textbf{assert} statement between
berghofe@45044: \textbf{while} and \textbf{loop} rather than directly after the \textbf{loop}.
berghofe@45044: In the former case, the loop invariant has to be proved only once, whereas in
berghofe@45044: the latter case, it has to be proved twice: since the \textbf{assert} occurs after
berghofe@45044: the check of the exit condition, the invariant has to be proved for the path
berghofe@45044: from the \textbf{assert} statement to the \textbf{assert} statement, and for
berghofe@45044: the path from the \textbf{assert} statement to the postcondition. In the case
berghofe@45044: of the \texttt{G\_C\_D} procedure, this might not seem particularly problematic,
berghofe@45044: since the proof of the invariant is very simple, but it can unnecessarily
berghofe@45044: complicate matters if the proof of the invariant is non-trivial. The simplified
berghofe@45044: program for computing the greatest common divisor, together with its correctness
berghofe@45044: proof, is shown in \figref{fig:simple-gcd-proof}. Since the package specification
berghofe@45044: has not changed, we only show the body of the packages. The two VCs can now be
berghofe@45044: proved by a single application of Isabelle's proof method @{text simp}.
berghofe@45044: *}
berghofe@45044:
berghofe@45044: (*<*)
berghofe@45044: end
berghofe@45044: (*>*)