proof.tex 3.38 KB
Newer Older
Benoit Viguier's avatar
Benoit Viguier committed
1
2
3
4
5
6
7
8
9
10
11
\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}

Benoit Viguier's avatar
Benoit Viguier committed
12

Benoit Viguier's avatar
Benoit Viguier committed
13
14
15
16
17
18
19
  % 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}};
Benoit Viguier's avatar
Benoit Viguier committed
20
    % \draw (1.25,0)  node[anchor=south east, inner sep=0pt] {\includegraphics[width=.0125\textwidth]{img/coq_logo.png}};
Benoit Viguier's avatar
Benoit Viguier committed
21
22
23
24
25
  \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;
Benoit Viguier's avatar
Benoit Viguier committed
26
    \draw (0,0) -- (2.5,0) -- (2.5,-1.25) -- (0, -1.25) -- cycle;
Benoit Viguier's avatar
Benoit Viguier committed
27
    \draw (0.3,-0.05) node[textstyle] {Proof};
Benoit Viguier's avatar
Benoit Viguier committed
28
29
    \draw (1.25,-0.5) node[textstyle, anchor=center] {\{{\color{doc@lstnumbers}\textbf{Pre}}\} \texttt{Prog} \{{\color{doc@lstdirective}\textbf{Post}}\}};
    \draw (2.5,-1.25) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{\checkmark}};
Benoit Viguier's avatar
Benoit Viguier committed
30
31
32
  \end{scope}

  % VST Spec
Benoit Viguier's avatar
Benoit Viguier committed
33
  \begin{scope}[yshift=-2.5 cm,xshift=3 cm]
Benoit Viguier's avatar
Benoit Viguier committed
34
35
36
37
    \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] {
Benoit Viguier's avatar
Benoit Viguier committed
38
      {\color{doc@lstnumbers}\textbf{Pre}}:\\
Benoit Viguier's avatar
Benoit Viguier committed
39
      ~~$n$, $P$\\
Benoit Viguier's avatar
Benoit Viguier committed
40
      {\color{doc@lstdirective}\textbf{Post}}:\\
Benoit Viguier's avatar
Benoit Viguier committed
41
42
43
44
      ~~\texttt{CSM}$(n,P)$};
  \end{scope}

  % Definition of CSM
Benoit Viguier's avatar
Benoit Viguier committed
45
  \begin{scope}[yshift=-4.5 cm,xshift=0 cm]
Benoit Viguier's avatar
Benoit Viguier committed
46
    \draw (0,0) -- (0.4, 0.4) -- (2,0.4) -- (2,0) -- cycle;
Benoit Viguier's avatar
Benoit Viguier committed
47
    \draw (0,0) -- (2,0) -- (2,-1) -- (0, -1) -- cycle;
Benoit Viguier's avatar
Benoit Viguier committed
48
    \draw (0.3,-0.05) node[textstyle] {Definition};
Benoit Viguier's avatar
Benoit Viguier committed
49
    \draw (1,-0.5) node[textstyle, anchor=center] {\texttt{CSM}};
Benoit Viguier's avatar
Benoit Viguier committed
50
51
52
  \end{scope}

  % Spec of Curve nP
Benoit Viguier's avatar
Benoit Viguier committed
53
  \begin{scope}[yshift=-7 cm,xshift=0 cm]
Benoit Viguier's avatar
Benoit Viguier committed
54
    \draw (0,0) -- (0.4, 0.4) -- (2,0.4) -- (2,0) -- cycle;
Benoit Viguier's avatar
Benoit Viguier committed
55
    \draw (0,0) -- (2,0) -- (2,-1) -- (0, -1) -- cycle;
Benoit Viguier's avatar
Benoit Viguier committed
56
    \draw (0.3,-0.05) node[textstyle] {Definition};
Benoit Viguier's avatar
Benoit Viguier committed
57
    \draw (1,-0.5) node[textstyle, anchor=center] {$[n]P$};
Benoit Viguier's avatar
Benoit Viguier committed
58
59
60
  \end{scope}

  % Correctness Theorem
Benoit Viguier's avatar
Benoit Viguier committed
61
  \begin{scope}[yshift=-6.5 cm,xshift=6 cm]
Benoit Viguier's avatar
Benoit Viguier committed
62
    \draw (0,0) -- (0.4, 0.4) -- (2.5,0.4) -- (2.5,0) -- cycle;
Benoit Viguier's avatar
Benoit Viguier committed
63
    \draw (0,0) -- (2.5,0) -- (2.5,-1.5) -- (0, -1.5) -- cycle;
Benoit Viguier's avatar
Benoit Viguier committed
64
    \draw (0.3,-0.05) node[textstyle] {Proof};
Benoit Viguier's avatar
Benoit Viguier committed
65
66
    \draw (2.5,-1.5) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{\checkmark}};
    \draw (1.25,-0.75) node[textstyle, anchor=center] {{\color{doc@lstnumbers}\textbf{Pre}} $\implies$\\$\text{\texttt{CSM}}(n,P) = [n]P$};
Benoit Viguier's avatar
Benoit Viguier committed
67
68
69
  \end{scope}

  \draw [very thick, ->] (1.25,-0.5) -- (2.5, -0.5);
Benoit Viguier's avatar
Benoit Viguier committed
70
71
72
73
74
  \draw [very thick, ->] (3.75,-0.5) -- (6, -0.5);
  \draw [very thick, ->] (5,-3.5) -- (6.5, -1.25);
  \draw [very thick, ->] (2,-5) -- (3, -3.5);
  \draw [very thick, ->] (2,-5) -- (6, -7);
  \draw [very thick, ->] (2,-7.5) -- (6, -7.5);
Benoit Viguier's avatar
Benoit Viguier committed
75
76

\end{tikzpicture}