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