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:exampleverification}

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:gcdprog}

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:gcdproof}

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:gcdprog},

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:gcdproof}.

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:gcdproof}, we start Isabelle with the command

berghofe@45044

51 
\begin{verbatim}

berghofe@45044

52 
isabelle emacs l HOLSPARK Greatest_Common_Divisor.thy

berghofe@45044

53 
\end{verbatim}

berghofe@45044

54 
The option ``\texttt{l HOLSPARK}'' 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 \<le> integer__size"}" \\

berghofe@45044

84 
and & @{text "g_c_d_rules6:"}\ "@{text "0 \<le> 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 \<le> 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 \<le> 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:gcdstatus}

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@45044

130 
\texttt{*.siv} or \texttt{*.vcg} 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:gcdstatus}.

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:provingvcs}

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 nonnegative 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 nonnegative when applied to a nonnegative 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 \<le> 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 nonnegative 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:simplegcdproof}

berghofe@45044

222 
\end{figure}

berghofe@45044

223 
When looking at the program from \figref{fig:gcdprog} 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 nonnegative by construction, the values computed by the algorithm

berghofe@45044

228 
are trivially proved to be nonnegative. Since we are working with nonnegative

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 nontrivial. 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:simplegcdproof}. 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 
(*>*)
