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