equal
deleted
inserted
replaced
74 \end{array}$} (post); |
74 \end{array}$} (post); |
75 \end{tikzpicture} |
75 \end{tikzpicture} |
76 \caption{Control flow graph for procedure \texttt{Proc2}} |
76 \caption{Control flow graph for procedure \texttt{Proc2}} |
77 \label{fig:proc2-graph} |
77 \label{fig:proc2-graph} |
78 \end{figure} |
78 \end{figure} |
79 As explained by Barnes @{cite \<open>\S 11.5\<close> Barnes}, the \SPARK{} Examiner unfolds the loop |
79 As explained by Barnes \<^cite>\<open>\<open>\S 11.5\<close> in Barnes\<close>, the \SPARK{} Examiner unfolds the loop |
80 \begin{lstlisting} |
80 \begin{lstlisting} |
81 for I in T range L .. U loop |
81 for I in T range L .. U loop |
82 --# assert P (I); |
82 --# assert P (I); |
83 S; |
83 S; |
84 end loop; |
84 end loop; |