45044
|
1 |
(*<*)
|
|
2 |
theory VC_Principles
|
|
3 |
imports Proc1 Proc2
|
|
4 |
begin
|
|
5 |
(*>*)
|
|
6 |
|
|
7 |
chapter {* Principles of VC generation *}
|
|
8 |
|
|
9 |
text {*
|
|
10 |
\label{sec:vc-principles}
|
|
11 |
In this section, we will discuss some aspects of VC generation that are
|
|
12 |
useful for understanding and optimizing the VCs produced by the \SPARK{}
|
|
13 |
Examiner.
|
|
14 |
|
|
15 |
\begin{figure}
|
|
16 |
\lstinputlisting{loop_invariant.ads}
|
|
17 |
\lstinputlisting{loop_invariant.adb}
|
|
18 |
\caption{Assertions in for-loops}
|
|
19 |
\label{fig:loop-invariant-ex}
|
|
20 |
\end{figure}
|
|
21 |
\begin{figure}
|
|
22 |
\begin{tikzpicture}
|
|
23 |
\tikzstyle{box}=[draw, drop shadow, fill=white, rounded corners]
|
|
24 |
\node[box] (pre) at (0,0) {precondition};
|
|
25 |
\node[box] (assn) at (0,-3) {assertion};
|
|
26 |
\node[box] (post) at (0,-6) {postcondition};
|
|
27 |
\draw[-latex] (pre) -- node [right] {\small$(1 - 1) * b \mod 2^{32} = 0$} (assn);
|
|
28 |
\draw[-latex] (assn) .. controls (2.5,-4.5) and (2.5,-1.5) .. %
|
|
29 |
node [right] {\small$\begin{array}{l} %
|
|
30 |
(i - 1) * b \mod 2^{32} = c ~\longrightarrow \\ %
|
|
31 |
(i + 1 - 1) * b \mod 2^{32} ~= \\ %
|
|
32 |
(c + b) \mod 2^{32} %
|
|
33 |
\end{array}$} (assn);
|
|
34 |
\draw[-latex] (assn) -- node [right] {\small$\begin{array}{l} %
|
|
35 |
(a - 1) * b \mod 2^{32} = c ~\longrightarrow \\ %
|
|
36 |
a * b \mod 2^{32} = (c + b) \mod 2^{32} %
|
|
37 |
\end{array}$} (post);
|
|
38 |
\draw[-latex] (pre) .. controls (-2,-3) .. %
|
|
39 |
node [left] {\small$\begin{array}{l} %
|
|
40 |
\neg 1 \le a ~\longrightarrow \\ %
|
|
41 |
a * b \mod 2^{32} = 0 %
|
|
42 |
\end{array}$} (post);
|
|
43 |
\end{tikzpicture}
|
|
44 |
\caption{Control flow graph for procedure \texttt{Proc1}}
|
|
45 |
\label{fig:proc1-graph}
|
|
46 |
\end{figure}
|
|
47 |
\begin{figure}
|
|
48 |
\begin{tikzpicture}
|
|
49 |
\tikzstyle{box}=[draw, drop shadow, fill=white, rounded corners]
|
|
50 |
\node[box] (pre) at (0,0) {precondition};
|
|
51 |
\node[box] (assn1) at (2,-3) {assertion 1};
|
|
52 |
\node[box] (assn2) at (2,-6) {assertion 2};
|
|
53 |
\node[box] (post) at (0,-9) {postcondition};
|
|
54 |
\draw[-latex] (pre) -- node [right] {\small$(1 - 1) * b \mod 2^{32} = 0$} (assn1);
|
|
55 |
\draw[-latex] (assn1) -- node [left] {\small$\begin{array}{l} %
|
|
56 |
(i - 1) * b \mod 2^{32} = c \\ %
|
|
57 |
\longrightarrow \\ %
|
|
58 |
i * b \mod 2^{32} = \\ %
|
|
59 |
(c + b) \mod 2^{32} %
|
|
60 |
\end{array}$} (assn2);
|
|
61 |
\draw[-latex] (assn2) .. controls (4.5,-7.5) and (4.5,-1.5) .. %
|
|
62 |
node [right] {\small$\begin{array}{l} %
|
|
63 |
i * b \mod 2^{32} = c ~\longrightarrow \\ %
|
|
64 |
(i + 1 - 1) * b \mod 2^{32} = c %
|
|
65 |
\end{array}$} (assn1);
|
|
66 |
\draw[-latex] (assn2) -- node [right] {\small$\begin{array}{l} %
|
|
67 |
a * b \mod 2^{32} = c ~\longrightarrow \\ %
|
|
68 |
a * b \mod 2^{32} = c %
|
|
69 |
\end{array}$} (post);
|
|
70 |
\draw[-latex] (pre) .. controls (-3,-3) and (-3,-6) .. %
|
|
71 |
node [left,very near start] {\small$\begin{array}{l} %
|
|
72 |
\neg 1 \le a ~\longrightarrow \\ %
|
|
73 |
a * b \mod 2^{32} = 0 %
|
|
74 |
\end{array}$} (post);
|
|
75 |
\end{tikzpicture}
|
|
76 |
\caption{Control flow graph for procedure \texttt{Proc2}}
|
|
77 |
\label{fig:proc2-graph}
|
|
78 |
\end{figure}
|
58622
|
79 |
As explained by Barnes @{cite \<open>\S 11.5\<close> Barnes}, the \SPARK{} Examiner unfolds the loop
|
45044
|
80 |
\begin{lstlisting}
|
|
81 |
for I in T range L .. U loop
|
|
82 |
--# assert P (I);
|
|
83 |
S;
|
|
84 |
end loop;
|
|
85 |
\end{lstlisting}
|
|
86 |
to
|
|
87 |
\begin{lstlisting}
|
|
88 |
if L <= U then
|
|
89 |
I := L;
|
|
90 |
loop
|
|
91 |
--# assert P (I);
|
|
92 |
S;
|
|
93 |
exit when I = U;
|
|
94 |
I := I + 1;
|
|
95 |
end loop;
|
|
96 |
end if;
|
|
97 |
\end{lstlisting}
|
|
98 |
Due to this treatment of for-loops, the user essentially has to prove twice that
|
|
99 |
\texttt{S} preserves the invariant \textit{\texttt{P}}, namely for
|
|
100 |
the path from the assertion to the assertion and from the assertion to the next cut
|
|
101 |
point following the loop. The preservation of the invariant has to be proved even
|
|
102 |
more often when the loop is followed by an if-statement. For trivial invariants,
|
|
103 |
this might not seem like a big problem, but in realistic applications, where invariants
|
|
104 |
are complex, this can be a major inconvenience. Often, the proofs of the invariant differ
|
|
105 |
only in a few variables, so it is tempting to just copy and modify existing proof scripts,
|
|
106 |
but this leads to proofs that are hard to maintain.
|
|
107 |
The problem of having to prove the invariant several times can be avoided by rephrasing
|
|
108 |
the above for-loop to
|
|
109 |
\begin{lstlisting}
|
|
110 |
for I in T range L .. U loop
|
|
111 |
--# assert P (I);
|
|
112 |
S;
|
|
113 |
--# assert P (I + 1)
|
|
114 |
end loop;
|
|
115 |
\end{lstlisting}
|
|
116 |
The VC for the path from the second assertion to the first assertion is trivial and can
|
|
117 |
usually be proved automatically by the \SPARK{} Simplifier, whereas the VC for the path
|
|
118 |
from the first assertion to the second assertion actually expresses the fact that
|
|
119 |
\texttt{S} preserves the invariant.
|
|
120 |
|
|
121 |
We illustrate this technique using the example package shown in \figref{fig:loop-invariant-ex}.
|
|
122 |
It contains two procedures \texttt{Proc1} and \texttt{Proc2}, both of which implement
|
|
123 |
multiplication via addition. The procedures have the same specification, but in \texttt{Proc1},
|
|
124 |
only one \textbf{assert} statement is placed at the beginning of the loop, whereas \texttt{Proc2}
|
|
125 |
employs the trick explained above.
|
|
126 |
After applying the \SPARK{} Simplifier to the VCs generated for \texttt{Proc1}, two very
|
|
127 |
similar VCs
|
|
128 |
@{thm [display] (concl) procedure_proc1_5 [simplified pow_2_32_simp]}
|
|
129 |
and
|
|
130 |
@{thm [display,margin=60] (concl) procedure_proc1_8 [simplified pow_2_32_simp]}
|
|
131 |
remain, whereas for \texttt{Proc2}, only the first of the above VCs remains.
|
|
132 |
Why placing \textbf{assert} statements both at the beginning and at the end of the loop body
|
|
133 |
simplifies the proof of the invariant should become obvious when looking at \figref{fig:proc1-graph}
|
|
134 |
and \figref{fig:proc2-graph} showing the \emph{control flow graphs} for \texttt{Proc1} and
|
|
135 |
\texttt{Proc2}, respectively. The nodes in the graph correspond to cut points in the program,
|
|
136 |
and the paths between the cut points are annotated with the corresponding VCs. To reduce the
|
|
137 |
size of the graphs, we do not show nodes and edges corresponding to runtime checks.
|
|
138 |
The VCs for the path bypassing the loop and for the path from the precondition to the
|
|
139 |
(first) assertion are the same for both procedures. The graph for \texttt{Proc1} contains
|
|
140 |
two VCs expressing that the invariant is preserved by the execution of the loop body: one
|
|
141 |
for the path from the assertion to the assertion, and another one for the path from the
|
|
142 |
assertion to the conclusion, which corresponds to the last iteration of the loop. The latter
|
|
143 |
VC can be obtained from the former by simply replacing $i$ by $a$. In contrast, the graph
|
|
144 |
for \texttt{Proc2} contains only one such VC for the path from assertion 1 to assertion 2.
|
|
145 |
The VC for the path from assertion 2 to assertion 1 is trivial, and so is the VC for the
|
|
146 |
path from assertion 2 to the postcondition, expressing that the loop invariant implies
|
|
147 |
the postcondition when the loop has terminated.
|
|
148 |
*}
|
|
149 |
|
|
150 |
(*<*)
|
|
151 |
end
|
|
152 |
(*>*)
|