src/HOL/SPARK/Manual/VC_Principles.thy
author huffman
Sun Apr 01 16:09:58 2012 +0200 (2012-04-01)
changeset 47255 30a1692557b0
parent 45044 2fae15f8984d
child 58622 aa99568f56de
permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
     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}
    79 As explained by Barnes \cite[\S 11.5]{Barnes}, the \SPARK{} Examiner unfolds the loop
    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 (*>*)