summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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

7 chapter {* Principles of VC generation *}

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.

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.

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 *}

150 (*<*)

151 end

152 (*>*)