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