1(*<*)
2theory VC_Principles
3imports Proc1 Proc2
4begin
5(*>*)
6
7chapter \<open>Principles of VC generation\<close>
8
9text \<open>
10\label{sec:vc-principles}
11In this section, we will discuss some aspects of VC generation that are
12useful for understanding and optimizing the VCs produced by the \SPARK{}
13Examiner.
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) .. %
29node [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 \\ %
36a * b \mod 2^{32} = (c + b) \mod 2^{32} %
37\end{array}$} (post);
38\draw[-latex] (pre) .. controls (-2,-3) .. %
39node [left] {\small$\begin{array}{l} %
40\neg 1 \le a ~\longrightarrow \\ %
41a * 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 \\ %
58i * 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) .. %
62node [right] {\small$\begin{array}{l} %
63i * 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} %
67a * b \mod 2^{32} = c ~\longrightarrow \\ %
68a * b \mod 2^{32} = c %
69\end{array}$} (post);
70\draw[-latex] (pre) .. controls (-3,-3) and (-3,-6) .. %
71node [left,very near start] {\small$\begin{array}{l} %
72\neg 1 \le a ~\longrightarrow \\ %
73a * 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}
79As explained by Barnes @{cite \<open>\S 11.5\<close> Barnes}, the \SPARK{} Examiner unfolds the loop
80\begin{lstlisting}
81for I in T range L .. U loop
82  --# assert P (I);
83  S;
84end loop;
85\end{lstlisting}
86to
87\begin{lstlisting}
88if 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;
96end if;
97\end{lstlisting}
98Due 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
100the path from the assertion to the assertion and from the assertion to the next cut
101point following the loop. The preservation of the invariant has to be proved even
102more often when the loop is followed by an if-statement. For trivial invariants,
103this might not seem like a big problem, but in realistic applications, where invariants
104are complex, this can be a major inconvenience. Often, the proofs of the invariant differ
105only in a few variables, so it is tempting to just copy and modify existing proof scripts,
106but this leads to proofs that are hard to maintain.
107The problem of having to prove the invariant several times can be avoided by rephrasing
108the above for-loop to
109\begin{lstlisting}
110for I in T range L .. U loop
111  --# assert P (I);
112  S;
113  --# assert P (I + 1)
114end loop;
115\end{lstlisting}
116The VC for the path from the second assertion to the first assertion is trivial and can
117usually be proved automatically by the \SPARK{} Simplifier, whereas the VC for the path
118from the first assertion to the second assertion actually expresses the fact that
119\texttt{S} preserves the invariant.
120
121We illustrate this technique using the example package shown in \figref{fig:loop-invariant-ex}.
122It contains two procedures \texttt{Proc1} and \texttt{Proc2}, both of which implement
123multiplication via addition. The procedures have the same specification, but in \texttt{Proc1},
124only one \textbf{assert} statement is placed at the beginning of the loop, whereas \texttt{Proc2}
125employs the trick explained above.
126After applying the \SPARK{} Simplifier to the VCs generated for \texttt{Proc1}, two very
127similar VCs
128@{thm [display] (concl) procedure_proc1_5 [simplified pow_2_32_simp]}
129and
130@{thm [display,margin=60] (concl) procedure_proc1_8 [simplified pow_2_32_simp]}
131remain, whereas for \texttt{Proc2}, only the first of the above VCs remains.
132Why placing \textbf{assert} statements both at the beginning and at the end of the loop body
133simplifies the proof of the invariant should become obvious when looking at \figref{fig:proc1-graph}
134and \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,
136and the paths between the cut points are annotated with the corresponding VCs. To reduce the
137size of the graphs, we do not show nodes and edges corresponding to runtime checks.
138The 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
140two VCs expressing that the invariant is preserved by the execution of the loop body: one
141for the path from the assertion to the assertion, and another one for the path from the
142assertion to the conclusion, which corresponds to the last iteration of the loop. The latter
143VC can be obtained from the former by simply replacing $i$ by $a$. In contrast, the graph
144for \texttt{Proc2} contains only one such VC for the path from assertion 1 to assertion 2.
145The VC for the path from assertion 2 to assertion 1 is trivial, and so is the VC for the
146path from assertion 2 to the postcondition, expressing that the loop invariant implies
147the postcondition when the loop has terminated.
148\<close>
149
150(*<*)
151end
152(*>*)
153