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;
     1 (*<*)

     2 theory VC_Principles

     3 imports Proc1 Proc2

     4 begin

     5 (*>*)

     6

     7 chapter \<open>Principles of VC generation\<close>

     8

     9 text \<open>

    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 \<open>\S 11.5\<close> 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 \<close>

   149

   150 (*<*)

   151 end

   152 (*>*)