proof.tex 3.07 KB
Newer Older
Benoit Viguier's avatar
Benoit Viguier committed
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}