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 \<open>Principles of VC generation\<close>
berghofe@45044
     8
wenzelm@63167
     9
text \<open>
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 \<open>\S 11.5\<close> 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
\<close>
berghofe@45044
   149
berghofe@45044
   150
(*<*)
berghofe@45044
   151
end
berghofe@45044
   152
(*>*)