Quelle VC_Principles.thy

Sprache: Isabelle

(*<*)
theory VC_Principles
imports Proc1 Proc2
begin
(*>*)

chapter ‹Principles of VC generation›

text ‹
label{sec:vc-principles}
this section, we will discuss some aspects of VC generation that are
for understanding and optimizing the VCs produced by the \SPARK{}
.

begin{figure}
lstinputlisting{loop_invariant.ads}
lstinputlisting{loop_invariant.adb}
caption{Assertions in for-loops}
label{fig:loop-invariant-ex}
end{figure}
begin{figure}
begin{tikzpicture}
tikzstyle{box}=[draw, drop shadow, fill=white, rounded corners]
node[box] (pre) at (0,0) {precondition};
node[box] (assn) at (0,-3) {assertion};
node[box] (post) at (0,-6) {postcondition};
draw[-latex] (pre) -- node [right] {\small$(1 - 1) * b \mod 2^{32} = 0$} (assn);
draw[-latex] (assn) .. controls (2.5,-4.5) and (2.5,-1.5) .. %
[right] {\small$\begin{array}{l} %
i - 1) * b \mod 2^{32} = c ~\longrightarrow \\ %
i + 1 - 1) * b \mod 2^{32} ~= \\ %
c + b) \mod 2^{32} %
end{array}$} (assn);
draw[-latex] (assn) -- node [right] {\small$\begin{array}{l} %
a - 1) * b \mod 2^{32} = c ~\longrightarrow \\ %
* b \mod 2^{32} = (c + b) \mod 2^{32} %
end{array}$} (post);
draw[-latex] (pre) .. controls (-2,-3) .. %
[left] {\small$\begin{array}{l} %
neg 1 \le a ~\longrightarrow \\ %
* b \mod 2^{32} = 0 %
end{array}$} (post);
end{tikzpicture}
caption{Control flow graph for procedure \texttt{Proc1}}
label{fig:proc1-graph}
end{figure}
begin{figure}
begin{tikzpicture}
tikzstyle{box}=[draw, drop shadow, fill=white, rounded corners]
node[box] (pre) at (0,0) {precondition};
node[box] (assn1) at (2,-3) {assertion 1};
node[box] (assn2) at (2,-6) {assertion 2};
node[box] (post) at (0,-9) {postcondition};
draw[-latex] (pre) -- node [right] {\small$(1 - 1) * b \mod 2^{32} = 0$} (assn1);
draw[-latex] (assn1) -- node [left] {\small$\begin{array}{l} %
i - 1) * b \mod 2^{32} = c \\ %
longrightarrow \\ %
* b \mod 2^{32} = \\ %
c + b) \mod 2^{32} %
end{array}$} (assn2);
draw[-latex] (assn2) .. controls (4.5,-7.5) and (4.5,-1.5) .. %
[right] {\small$\begin{array}{l} %
* b \mod 2^{32} = c ~\longrightarrow \\ %
i + 1 - 1) * b \mod 2^{32} = c %
end{array}$} (assn1);
draw[-latex] (assn2) -- node [right] {\small$\begin{array}{l} %
* b \mod 2^{32} = c ~\longrightarrow \\ %
* b \mod 2^{32} = c %
end{array}$} (post);
draw[-latex] (pre) .. controls (-3,-3) and (-3,-6) .. %
[left,very near start] {\small$\begin{array}{l} %
neg 1 \le a ~\longrightarrow \\ %
* b \mod 2^{32} = 0 %
end{array}$} (post);
end{tikzpicture}
caption{Control flow graph for procedure \texttt{Proc2}}
label{fig:proc2-graph}
end{figure}
explained by Barnes cite‹‹\S 11.5› in Barnes›, the \SPARK{} Examiner unfolds the loop
begin{lstlisting}
I in T range L .. U loop
--# assert P (I);
S;
loop;
end{lstlisting}

begin{lstlisting}
L <= U then
I := L;
loop
--# assert P (I);
S;
exit when I = U;
I := I + 1;
end loop;
if;
end{lstlisting}
to this treatment of for-loops, the user essentially has to prove twice that
texttt{S} preserves the invariant \textit{\texttt{P}}, namely for
path from the assertion to the assertion and from the assertion to the next cut
following the loop. The preservation of the invariant has to be proved even
often when the loop is followed by an if-statement. For trivial invariants,
might not seem like a big problem, but in realistic applications, where invariants
complex, this can be a major inconvenience. Often, the proofs of the invariant differ
in a few variables, so it is tempting to just copy and modify existing proof scripts,
this leads to proofs that are hard to maintain.
problem of having to prove the invariant several times can be avoided by rephrasing
above for-loop to
begin{lstlisting}
I in T range L .. U loop
--# assert P (I);
S;
--# assert P (I + 1)
loop;
end{lstlisting}
VC for the path from the second assertion to the first assertion is trivial and can
be proved automatically by the \SPARK{} Simplifier, whereas the VC for the path
the first assertion to the second assertion actually expresses the fact that
texttt{S} preserves the invariant.

illustrate this technique using the example package shown in \figref{fig:loop-invariant-ex}.
contains two procedures \texttt{Proc1} and \texttt{Proc2}, both of which implement
via addition. The procedures have the same specification, but in \texttt{Proc1},
one \textbf{assert} statement is placed at the beginning of the loop, whereas \texttt{Proc2}
the trick explained above.
applying the \SPARK{} Simplifier to the VCs generated for \texttt{Proc1}, two very
VCs
{thm [display] (concl) procedure_proc1_5 [simplified pow_2_32_simp]}

{thm [display,margin=60] (concl) procedure_proc1_8 [simplified pow_2_32_simp]}
, whereas for \texttt{Proc2}, only the first of the above VCs remains.
placing \textbf{assert} statements both at the beginning and at the end of the loop body
the proof of the invariant should become obvious when looking at \figref{fig:proc1-graph}
\figref{fig:proc2-graph} showing the \emph{control flow graphs} for \texttt{Proc1} and
texttt{Proc2}, respectively. The nodes in the graph correspond to cut points in the program,
the paths between the cut points are annotated with the corresponding VCs. To reduce the
of the graphs, we do not show nodes and edges corresponding to runtime checks.
VCs for the path bypassing the loop and for the path from the precondition to the
first) assertion are the same for both procedures. The graph for \texttt{Proc1} contains
VCs expressing that the invariant is preserved by the execution of the loop body: one
the path from the assertion to the assertion, and another one for the path from the
to the conclusion, which corresponds to the last iteration of the loop. The latter
can be obtained from the former by simply replacing $i$ by $a$. In contrast, the graph
\texttt{Proc2} contains only one such VC for the path from assertion 1 to assertion 2.
VC for the path from assertion 2 to assertion 1 is trivial, and so is the VC for the
from assertion 2 to the postcondition, expressing that the loop invariant implies
postcondition when the loop has terminated.
›

(*<*)
end
(*>*)

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-06-30) ¤

Wurzel

Suchen

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.