berghofe@45044

1 
(*<*)

berghofe@45044

2 
theory Example_Verification

wenzelm@66453

3 
imports "HOLSPARKExamples.Greatest_Common_Divisor" Simple_Greatest_Common_Divisor

berghofe@45044

4 
begin

berghofe@45044

5 
(*>*)

berghofe@45044

6 

wenzelm@63167

7 
chapter \<open>Verifying an Example Program\<close>

berghofe@45044

8 

wenzelm@63167

9 
text \<open>

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

wenzelm@58622

26 
which has been taken from the book about \SPARK{} by Barnes @{cite \<open>\S 11.6\<close> Barnes}.

wenzelm@63167

27 
\<close>

berghofe@45044

28 

wenzelm@63167

29 
section \<open>Importing \SPARK{} VCs into Isabelle\<close>

berghofe@45044

30 

wenzelm@63167

31 
text \<open>

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}

wenzelm@63167

79 
fixes & \<open>m ::\<close>\ "\<open>int\<close>" \\

wenzelm@63167

80 
and & \<open>n ::\<close>\ "\<open>int\<close>" \\

wenzelm@63167

81 
and & \<open>c ::\<close>\ "\<open>int\<close>" \\

wenzelm@63167

82 
and & \<open>d ::\<close>\ "\<open>int\<close>" \\

wenzelm@63167

83 
assumes & \<open>g_c_d_rules1:\<close>\ "\<open>0 \<le> integer__size\<close>" \\

wenzelm@63167

84 
and & \<open>g_c_d_rules6:\<close>\ "\<open>0 \<le> natural__size\<close>" \\

berghofe@45044

85 
\multicolumn{2}{l}{notes definition} \\

wenzelm@63167

86 
\multicolumn{2}{l}{\hspace{2ex}\<open>defns =\<close>\ `\<open>integer__first =  2147483648\<close>`} \\

wenzelm@63167

87 
\multicolumn{2}{l}{\hspace{4ex}`\<open>integer__last = 2147483647\<close>`} \\

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}

wenzelm@63167

94 
\<open>g_c_d_rules2:\<close> & \<open>integer__first =  2147483648\<close> \\

wenzelm@63167

95 
\<open>g_c_d_rules3:\<close> & \<open>integer__last = 2147483647\<close> \\

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 
\ \\

wenzelm@63167

103 
\<open>procedure_g_c_d_4\<close>\ (unproved) \\

berghofe@45044

104 
\ \ \begin{tabular}{ll}

wenzelm@63167

105 
assumes & \<open>H1:\<close>\ "\<open>0 \<le> c\<close>" \\

wenzelm@63167

106 
and & \<open>H2:\<close>\ "\<open>0 < d\<close>" \\

wenzelm@63167

107 
and & \<open>H3:\<close>\ "\<open>gcd c d = gcd m n\<close>" \\

berghofe@45044

108 
\dots \\

wenzelm@63167

109 
shows & "\<open>0 < c  c sdiv d * d\<close>" \\

wenzelm@63167

110 
and & "\<open>gcd d (c  c sdiv d * d) = gcd m n\<close>

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 
\ \\

wenzelm@63167

115 
\<open>procedure_g_c_d_11\<close>\ (unproved) \\

berghofe@45044

116 
\ \ \begin{tabular}{ll}

wenzelm@63167

117 
assumes & \<open>H1:\<close>\ "\<open>0 \<le> c\<close>" \\

wenzelm@63167

118 
and & \<open>H2:\<close>\ "\<open>0 < d\<close>" \\

wenzelm@63167

119 
and & \<open>H3:\<close>\ "\<open>gcd c d = gcd m n\<close>" \\

berghofe@45044

120 
\dots \\

wenzelm@63167

121 
shows & "\<open>d = gcd m n\<close>"

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@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: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.

wenzelm@63167

142 
\<close>

berghofe@45044

143 

wenzelm@63167

144 
section \<open>Proving the VCs\<close>

berghofe@45044

145 

wenzelm@63167

146 
text \<open>

berghofe@45044

147 
\label{sec:provingvcs}

wenzelm@63167

148 
The two open VCs are \<open>procedure_g_c_d_4\<close> and \<open>procedure_g_c_d_11\<close>,

wenzelm@63167

149 
both of which contain the \<open>gcd\<close> 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

wenzelm@63167

155 
\<open>?C1\<close>, \<open>?C2\<close>, etc. If there is just one conclusion, it can

wenzelm@63167

156 
also be referenced by \<open>?thesis\<close>. It is important to note that the

wenzelm@63167

157 
\texttt{div} operator of FDL behaves differently from the \<open>div\<close> 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

wenzelm@63167

160 
\texttt{div} operator is mapped to the \<open>sdiv\<close> 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}.

wenzelm@63167

166 
For nonnegative dividend and divisor, \<open>sdiv\<close> is equivalent to \<open>div\<close>,

wenzelm@63167

167 
as witnessed by theorem \<open>sdiv_pos_pos\<close>:

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}

wenzelm@63167

172 
just becomes \<open>c  c sdiv d * d\<close> in Isabelle. The first conclusion of

wenzelm@63167

173 
\<open>procedure_g_c_d_4\<close> requires us to prove that the remainder of \<open>c\<close>

wenzelm@63167

174 
and \<open>d\<close> is greater than \<open>0\<close>. To do this, we use the theorem

haftmann@64246

175 
\<open>minus_div_mult_eq_mod [symmetric]\<close> describing the correspondence between \<open>div\<close>

wenzelm@63167

176 
and \<open>mod\<close>

haftmann@64246

177 
@{thm [display] minus_div_mult_eq_mod [symmetric]}

wenzelm@63167

178 
together with the theorem \<open>pos_mod_sign\<close> saying that the result of the

wenzelm@63167

179 
\<open>mod\<close> operator is nonnegative when applied to a nonnegative divisor:

berghofe@45044

180 
@{thm [display] pos_mod_sign}

wenzelm@63167

181 
We will also need the aforementioned theorem \<open>sdiv_pos_pos\<close> in order for

wenzelm@63167

182 
the standard Isabelle/HOL theorems about \<open>div\<close> to be applicable

wenzelm@63167

183 
to the VC, which is formulated using \<open>sdiv\<close> rather that \<open>div\<close>.

wenzelm@63167

184 
Note that the proof uses \texttt{`\<open>0 \<le> c\<close>`} and \texttt{`\<open>0 < d\<close>`}

wenzelm@63167

185 
rather than \<open>H1\<close> and \<open>H2\<close> 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.

wenzelm@63167

189 
Moreover, proof scripts using abbreviations like \<open>H1\<close> and \<open>H2\<close>

berghofe@45044

190 
are hard to read without assistance from Isabelle.

wenzelm@63167

191 
The second conclusion of \<open>procedure_g_c_d_4\<close> requires us to prove that

wenzelm@63167

192 
the \<open>gcd\<close> of \<open>d\<close> and the remainder of \<open>c\<close> and \<open>d\<close>

wenzelm@63167

193 
is equal to the \<open>gcd\<close> of the original input values \<open>m\<close> and \<open>n\<close>,

berghofe@45044

194 
which is the actual \emph{invariant} of the procedure. This is a consequence

wenzelm@63167

195 
of theorem \<open>gcd_non_0_int\<close>

berghofe@45044

196 
@{thm [display] gcd_non_0_int}

haftmann@64246

197 
Again, we also need theorems \<open>minus_div_mult_eq_mod [symmetric]\<close> and \<open>sdiv_pos_pos\<close>

berghofe@45044

198 
to justify that \SPARK{}'s \textbf{rem} operator is equivalent to Isabelle's

wenzelm@63167

199 
\<open>mod\<close> operator for nonnegative operands.

wenzelm@63167

200 
The VC \<open>procedure_g_c_d_11\<close> 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

wenzelm@63167

203 
of \<open>c\<close> and \<open>d\<close>, and hence \<open>c mod d\<close> is \<open>0\<close> when exiting

wenzelm@63167

204 
the loop. This implies that \<open>gcd c d = d\<close>, since \<open>c\<close> is divisible

wenzelm@63167

205 
by \<open>d\<close>, so the conclusion follows using the assumption \<open>gcd c d = gcd m n\<close>.

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.

wenzelm@63167

212 
\<close>

berghofe@45044

213 

wenzelm@63167

214 
section \<open>Optimizing the proof\<close>

berghofe@45044

215 

wenzelm@63167

216 
text \<open>

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

haftmann@64246

230 
\textbf{rem}, which spares us an application of theorems \<open>minus_div_mult_eq_mod [symmetric]\<close>

wenzelm@63167

231 
and \<open>sdiv_pos_pos\<close>. Finally, as noted by Barnes @{cite \<open>\S 11.5\<close> 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

wenzelm@63167

245 
proved by a single application of Isabelle's proof method \<open>simp\<close>.

wenzelm@63167

246 
\<close>

berghofe@45044

247 

berghofe@45044

248 
(*<*)

berghofe@45044

249 
end

berghofe@45044

250 
(*>*)
