src/HOL/SPARK/Manual/Example_Verification.thy
 author berghofe Wed Apr 30 15:43:44 2014 +0200 (2014-04-30) changeset 56798 939e88e79724 parent 45044 2fae15f8984d child 58622 aa99568f56de permissions -rw-r--r--
Discontinued old spark_open; spark_open_siv is now spark_open
 berghofe@45044  1 (*<*)  berghofe@45044  2 theory Example_Verification  berghofe@45044  3 imports "../Examples/Gcd/Greatest_Common_Divisor" Simple_Greatest_Common_Divisor  berghofe@45044  4 begin  berghofe@45044  5 (*>*)  berghofe@45044  6 berghofe@45044  7 chapter {* Verifying an Example Program *}  berghofe@45044  8 berghofe@45044  9 text {*  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},  berghofe@45044  26 which has been taken from the book about \SPARK{} by Barnes \cite[\S 11.6]{Barnes}.  berghofe@45044  27 *}  berghofe@45044  28 berghofe@45044  29 section {* Importing \SPARK{} VCs into Isabelle *}  berghofe@45044  30 berghofe@45044  31 text {*  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}  berghofe@45044  79 fixes & @{text "m ::"}\ "@{text int}" \\  berghofe@45044  80 and & @{text "n ::"}\ "@{text int}" \\  berghofe@45044  81 and & @{text "c ::"}\ "@{text int}" \\  berghofe@45044  82 and & @{text "d ::"}\ "@{text int}" \\  berghofe@45044  83 assumes & @{text "g_c_d_rules1:"}\ "@{text "0 \ integer__size"}" \\  berghofe@45044  84 and & @{text "g_c_d_rules6:"}\ "@{text "0 \ natural__size"}" \\  berghofe@45044  85 \multicolumn{2}{l}{notes definition} \\  berghofe@45044  86 \multicolumn{2}{l}{\hspace{2ex}@{text "defns ="}\ @{text "integer__first = - 2147483648"}} \\  berghofe@45044  87 \multicolumn{2}{l}{\hspace{4ex}@{text "integer__last = 2147483647"}} \\  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}  berghofe@45044  94 @{text "g_c_d_rules2:"} & @{text "integer__first = - 2147483648"} \\  berghofe@45044  95 @{text "g_c_d_rules3:"} & @{text "integer__last = 2147483647"} \\  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 \ \\  berghofe@45044  103 @{text procedure_g_c_d_4}\ (unproved) \\  berghofe@45044  104 \ \ \begin{tabular}{ll}  berghofe@45044  105 assumes & @{text "H1:"}\ "@{text "0 \ c"}" \\  berghofe@45044  106 and & @{text "H2:"}\ "@{text "0 < d"}" \\  berghofe@45044  107 and & @{text "H3:"}\ "@{text "gcd c d = gcd m n"}" \\  berghofe@45044  108 \dots \\  berghofe@45044  109 shows & "@{text "0 < c - c sdiv d * d"}" \\  berghofe@45044  110 and & "@{text "gcd d (c - c sdiv d * d) = gcd m n"}  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 \ \\  berghofe@45044  115 @{text procedure_g_c_d_11}\ (unproved) \\  berghofe@45044  116 \ \ \begin{tabular}{ll}  berghofe@45044  117 assumes & @{text "H1:"}\ "@{text "0 \ c"}" \\  berghofe@45044  118 and & @{text "H2:"}\ "@{text "0 < d"}" \\  berghofe@45044  119 and & @{text "H3:"}\ "@{text "gcd c d = gcd m n"}" \\  berghofe@45044  120 \dots \\  berghofe@45044  121 shows & "@{text "d = gcd m n"}"  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.  berghofe@45044  142 *}  berghofe@45044  143 berghofe@45044  144 section {* Proving the VCs *}  berghofe@45044  145 berghofe@45044  146 text {*  berghofe@45044  147 \label{sec:proving-vcs}  berghofe@45044  148 The two open VCs are @{text procedure_g_c_d_4} and @{text procedure_g_c_d_11},  berghofe@45044  149 both of which contain the @{text gcd} 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  berghofe@45044  155 @{text "?C1"}, @{text "?C2"}, etc. If there is just one conclusion, it can  berghofe@45044  156 also be referenced by @{text "?thesis"}. It is important to note that the  berghofe@45044  157 \texttt{div} operator of FDL behaves differently from the @{text div} 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  berghofe@45044  160 \texttt{div} operator is mapped to the @{text sdiv} 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}.  berghofe@45044  166 For non-negative dividend and divisor, @{text sdiv} is equivalent to @{text div},  berghofe@45044  167 as witnessed by theorem @{text sdiv_pos_pos}:  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}  berghofe@45044  172 just becomes @{text "c - c sdiv d * d"} in Isabelle. The first conclusion of  berghofe@45044  173 @{text procedure_g_c_d_4} requires us to prove that the remainder of @{text c}  berghofe@45044  174 and @{text d} is greater than @{text 0}. To do this, we use the theorem  berghofe@45044  175 @{text zmod_zdiv_equality'} describing the correspondence between @{text div}  berghofe@45044  176 and @{text mod}  berghofe@45044  177 @{thm [display] zmod_zdiv_equality'}  berghofe@45044  178 together with the theorem @{text pos_mod_sign} saying that the result of the  berghofe@45044  179 @{text mod} operator is non-negative when applied to a non-negative divisor:  berghofe@45044  180 @{thm [display] pos_mod_sign}  berghofe@45044  181 We will also need the aforementioned theorem @{text sdiv_pos_pos} in order for  berghofe@45044  182 the standard Isabelle/HOL theorems about @{text div} to be applicable  berghofe@45044  183 to the VC, which is formulated using @{text sdiv} rather that @{text div}.  berghofe@45044  184 Note that the proof uses \texttt{@{text "0 \ c"}} and \texttt{@{text "0 < d"}}  berghofe@45044  185 rather than @{text H1} and @{text H2} 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.  berghofe@45044  189 Moreover, proof scripts using abbreviations like @{text H1} and @{text H2}  berghofe@45044  190 are hard to read without assistance from Isabelle.  berghofe@45044  191 The second conclusion of @{text procedure_g_c_d_4} requires us to prove that  berghofe@45044  192 the @{text gcd} of @{text d} and the remainder of @{text c} and @{text d}  berghofe@45044  193 is equal to the @{text gcd} of the original input values @{text m} and @{text n},  berghofe@45044  194 which is the actual \emph{invariant} of the procedure. This is a consequence  berghofe@45044  195 of theorem @{text gcd_non_0_int}  berghofe@45044  196 @{thm [display] gcd_non_0_int}  berghofe@45044  197 Again, we also need theorems @{text zmod_zdiv_equality'} and @{text sdiv_pos_pos}  berghofe@45044  198 to justify that \SPARK{}'s \textbf{rem} operator is equivalent to Isabelle's  berghofe@45044  199 @{text mod} operator for non-negative operands.  berghofe@45044  200 The VC @{text procedure_g_c_d_11} 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  berghofe@45044  203 of @{text c} and @{text d}, and hence @{text "c mod d"} is @{text 0} when exiting  berghofe@45044  204 the loop. This implies that @{text "gcd c d = d"}, since @{text c} is divisible  berghofe@45044  205 by @{text d}, so the conclusion follows using the assumption @{text "gcd c d = gcd m n"}.  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.  berghofe@45044  212 *}  berghofe@45044  213 berghofe@45044  214 section {* Optimizing the proof *}  berghofe@45044  215 berghofe@45044  216 text {*  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  berghofe@45044  230 \textbf{rem}, which spares us an application of theorems @{text zmod_zdiv_equality'}  berghofe@45044  231 and @{text sdiv_pos_pos}. Finally, as noted by Barnes \cite[\S 11.5]{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  berghofe@45044  245 proved by a single application of Isabelle's proof method @{text simp}.  berghofe@45044  246 *}  berghofe@45044  247 berghofe@45044  248 (*<*)  berghofe@45044  249 end  berghofe@45044  250 (*>*)