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