proof.tex 3.07 KB
 Benoit Viguier committed Jul 12, 2019 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 \begin{tikzpicture}[textstyle/.style={black, anchor= south west, align=center, minimum height=0.45cm, text centered, font=\scriptsize}] % C code \begin{scope}[yshift=0 cm,xshift=0 cm] \draw (0,0) -- (0.4, 0.4) -- (1.25,0.4) -- (1.25,0) -- cycle; \draw (0,0) -- (1.25,0) -- (1.25,-1.25) -- (0, -1.25) -- cycle; \draw (0.3,-0.05) node[textstyle] {code}; \draw (0.675,-0.5) node[textstyle, anchor=center] {\texttt{Prog}}; \draw (1.25,-1.25) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{.C}}; \end{scope} % V code \begin{scope}[yshift=0 cm,xshift=2.5 cm] \draw (0,0) -- (0.4, 0.4) -- (1.25,0.4) -- (1.25,0) -- cycle; \draw (0,0) -- (1.25,0) -- (1.25,-1.25) -- (0, -1.25) -- cycle; \draw (0.3,-0.05) node[textstyle] {code}; \draw (0.675,-0.5) node[textstyle, anchor=center] {\texttt{Prog}}; \draw (1.25,-1.25) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{.V}}; \end{scope} % VST Theorem \begin{scope}[yshift=0 cm,xshift=6 cm] \draw (0,0) -- (0.4, 0.4) -- (2.5,0.4) -- (2.5,0) -- cycle; \draw (0,0) -- (2.5,0) -- (2.5,-2) -- (0, -2) -- cycle; \draw (0.3,-0.05) node[textstyle] {Proof}; \draw (1.25,-1) node[textstyle, anchor=center] {\{Pre\} \texttt{Prog} \{Post\}}; \draw (2.5,-2) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{\checkmark}}; \end{scope} % VST Spec \begin{scope}[yshift=-3 cm,xshift=3 cm] \draw (0,0) -- (0.4, 0.4) -- (2,0.4) -- (2,0) -- cycle; \draw (0,0) -- (2,0) -- (2,-2) -- (0, -2) -- cycle; \draw (0.3,-0.05) node[textstyle] {Specification}; \draw (1,-1) node[textstyle, anchor=center, align=left] { Pre:\\ ~~$n$, $P$\\ Post:\\ ~~\texttt{CSM}$(n,P)$}; \end{scope} % Definition of CSM \begin{scope}[yshift=-6 cm,xshift=0 cm] \draw (0,0) -- (0.4, 0.4) -- (2,0.4) -- (2,0) -- cycle; \draw (0,0) -- (2,0) -- (2,-2) -- (0, -2) -- cycle; \draw (0.3,-0.05) node[textstyle] {Definition}; \draw (1,-1) node[textstyle, anchor=center] {\texttt{CSM}}; \end{scope} % Spec of Curve nP \begin{scope}[yshift=-9 cm,xshift=0 cm] \draw (0,0) -- (0.4, 0.4) -- (2,0.4) -- (2,0) -- cycle; \draw (0,0) -- (2,0) -- (2,-2) -- (0, -2) -- cycle; \draw (0.3,-0.05) node[textstyle] {Definition}; \draw (1,-1) node[textstyle, anchor=center] {$[n]P$}; \end{scope} % Correctness Theorem \begin{scope}[yshift=-7 cm,xshift=6 cm] \draw (0,0) -- (0.4, 0.4) -- (2.5,0.4) -- (2.5,0) -- cycle; \draw (0,0) -- (2.5,0) -- (2.5,-2) -- (0, -2) -- cycle; \draw (0.3,-0.05) node[textstyle] {Proof}; \draw (2.5,-2) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{\checkmark}}; \draw (1.25,-1) node[textstyle, anchor=center] {Pre $\implies$\\$\text{\texttt{CSM}}(n,P) = [n]P$}; \end{scope} \draw [very thick, ->] (1.25,-0.5) -- (2.5, -0.5); \draw [very thick, ->] (3.75,-0.5) -- (6, -1); \draw [very thick, ->] (5,-4) -- (6.5, -2); \draw [very thick, ->] (2,-6.5) -- (3.5, -5); \draw [very thick, ->] (2,-7.5) -- (6, -7.75); \draw [very thick, ->] (2,-10) -- (6, -8.25); \end{tikzpicture}