source: Papers/jar-cerco-2017/cerco.tex

Last change on this file was 3669, checked in by campbell, 3 years ago

Add some notes on specification

File size: 25.2 KB
Line 
1\begin{filecontents*}{example.eps}
2%!PS-Adobe-3.0 EPSF-3.0
3%%BoundingBox: 19 19 221 221
4%%CreationDate: Mon Sep 29 1997
5%%Creator: programmed by hand (JK)
6%%EndComments
7gsave
8newpath
9  20 20 moveto
10  20 220 lineto
11  220 220 lineto
12  220 20 lineto
13closepath
142 setlinewidth
15gsave
16  .4 setgray fill
17grestore
18stroke
19grestore
20\end{filecontents*}
21
22\RequirePackage{fix-cm}
23
24\documentclass[smallextended]{svjour3}
25
26\usepackage{amsfonts}
27\usepackage{amsmath}
28\usepackage{amssymb}
29\usepackage{array}
30\usepackage[british]{babel}
31\usepackage{color}
32\usepackage{enumerate}
33\usepackage{fancybox}
34\usepackage{fancyvrb}
35\usepackage{graphicx}
36\usepackage[colorlinks,
37            bookmarks,bookmarksopen,bookmarksdepth=2]{hyperref}
38\usepackage{hyphenat}
39\usepackage[utf8x]{inputenc}
40\usepackage{listings}
41\usepackage{mdwlist}
42\usepackage{microtype}
43\usepackage{multirow}
44\usepackage{stmaryrd}
45\usepackage{url}
46\usepackage[all]{xy}
47
48\usepackage{tikz}
49\usetikzlibrary{positioning,calc,patterns,chains,shapes.geometric,scopes}
50
51\lstset{language=C,basicstyle=\tt,basewidth=.5em,lineskip=-1.5pt}
52\def\lstlanguagefiles{lst-grafite.tex}
53
54\newlength{\mylength}
55\newenvironment{frametxt}%
56        {\setlength{\fboxsep}{5pt}
57                \setlength{\mylength}{\linewidth}%
58                \addtolength{\mylength}{-2\fboxsep}%
59                \addtolength{\mylength}{-2\fboxrule}%
60                \Sbox
61                \minipage{\mylength}%
62                        \setlength{\abovedisplayskip}{0pt}%
63                        \setlength{\belowdisplayskip}{0pt}%
64                }%
65                {\endminipage\endSbox
66                        \[\fbox{\TheSbox}\]}
67
68\smartqed
69
70\lstset{extendedchars=false}
71\lstset{inputencoding=utf8x}
72\DeclareUnicodeCharacter{8797}{:=}
73\DeclareUnicodeCharacter{10746}{++}
74\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
75\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
76
77\newcolumntype{b}{@{}>{{}}}
78\newcolumntype{B}{@{}>{{}}c<{{}}@{}}
79\newcolumntype{h}[1]{@{\hspace{#1}}}
80\newcolumntype{L}{>{$}l<{$}}
81\newcolumntype{C}{>{$}c<{$}}
82\newcolumntype{R}{>{$}r<{$}}
83\newcolumntype{S}{>{$(}r<{)$}}
84\newcolumntype{n}{@{}}
85\newcommand{\spanr}[2]{\multicolumn{1}{Rn}{\multirow{#1}{*}{(#2)}}}
86\def\nocol{\multicolumn{1}{ncn}{}}
87
88\newcommand{\cerco}{CerCo}
89\newcommand{\ocaml}{OCaml}
90\newcommand{\clight}{Clight}
91\newcommand{\matita}{Matita}
92\newcommand{\sdcc}{\texttt{sdcc}}
93
94\newcommand{\tern}[3]{#1\mathrel ? #2 : #3}
95\newcommand{\sop}[1]{\s{#1}\ }
96\newcommand{\sbin}[1]{\ \s{#1}\ }
97\newcommand{\Ell}{\mathcal L}
98\newcommand{\alphab}{\boldsymbol\alpha}
99\newcommand{\betab}{\boldsymbol\beta}
100\newcommand{\gramm}{\mathrel{::=}}
101\newcommand{\ass}{\mathrel{:=}}
102
103\renewcommand{\to}[1][]{\stackrel{#1}{\rightarrow}}
104
105\newcommand{\eg}{\emph{e.g.\ }}
106\newcommand{\ie}{\emph{i.e.\ }}
107
108\newcommand{\inde}{\hspace{20pt}}
109
110\usetikzlibrary{decorations.pathreplacing}
111\newcommand{\tikztarget}[2]{%
112  \tikz[remember picture, baseline={(#1.base)}]{
113  \node (#1) [inner sep = 0pt]{#2};}}
114\newcommand{\tikztargetm}[2]{%
115  \tikz[remember picture, baseline={(#1.base)}]{
116  \node (#1) [inner sep = 0pt]{$#2$};}}
117 
118  \newenvironment{comment}{{\bf MORE WORK:}} 
119 
120\newenvironment{restate-proposition}[2][{}]{\noindent\textbf{Proposition~{#2}}
121\;\textbf{#1}\  
122}{\vskip 1em} 
123 
124\newenvironment{restate-theorem}[2][{}]{\noindent\textbf{Theorem~{#2}}\;\textbf{
125#1}\  
126}{\vskip 1em} 
127 
128\newenvironment{restate-corollary}[2][{}]{\noindent\textbf{Corollary~{#2}}
129\;\textbf{#1}\  
130}{\vskip 1em} 
131 
132\newcommand{\myparagraph}[1]{\medskip\noindent\textbf{#1}} 
133 
134\newcommand{\Proofitemb}[1]{\medskip \noindent {\bf #1\;}} 
135\newcommand{\Proofitemfb}[1]{\noindent {\bf #1\;}} 
136\newcommand{\Proofitem}[1]{\medskip \noindent $#1\;$} 
137\newcommand{\Proofitemf}[1]{\noindent $#1\;$} 
138\newcommand{\Defitem}[1]{\smallskip \noindent $#1\;$} 
139\newcommand{\Defitemt}[1]{\smallskip \noindent {\em #1\;}} 
140\newcommand{\Defitemf}[1]{\noindent $#1\;$} 
141 
142 
143%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
144%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
145 
146 
147 
148%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
149%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
150 
151\newcommand{\eqdef}{=_{\text{def}}} 
152\newcommand{\concat}{\cdot}%%{\mathbin{+}}
153\newcommand{\Int}{\mathit{int}} 
154\newcommand{\nat}{\mathit{nat}} 
155\newcommand{\String}{\mathit{string}} 
156\newcommand{\Ident}{\mathit{ident}} 
157\newcommand{\Block}{\mathit{block}} 
158\newcommand{\Signature}{\mathit{signature}} 
159 
160\newcommand{\pc}{\mathit{pc}} 
161\newcommand{\estack}{\mathit{estack}} 
162\newcommand{\Error}{\epsilon} 
163 
164%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
165%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
166 
167% --------------------------------------------------------------------- %
168% Proof rule.                                                           %
169% --------------------------------------------------------------------- %
170 
171\newcommand{\staterule}[3]{%
172  $\begin{array}{@{}l}%
173   \mbox{#1}\\%
174   \begin{array}{c}
175   #2\\ 
176   \hline 
177   \raisebox{0ex}[2.5ex]{\strut}#3%
178   \end{array}
179  \end{array}$} 
180 
181\newcommand{\GAP}{2ex} 
182 
183\newcommand{\recall}[2]{%
184 $\begin{array}{c}
185 #1\\ 
186 \hline 
187 \raisebox{0ex}[2.5ex]{\strut}#2%
188 \end{array}$} 
189 
190\newcommand{\hbra}{\noindent\hbox to \textwidth{\leaders\hrule height1.8mm
191depth-1.5mm\hfill}} 
192\newcommand{\hket}{\noindent\hbox to \textwidth{\leaders\hrule
193height0.3mm\hfill}} 
194\newcommand{\ratio}{.3} 
195 
196\newenvironment{display}[1]{\begin{tabbing} 
197  \hspace{1.5em} \= \hspace{\ratio\linewidth-1.5em} \= \hspace{1.5em} \= \kill 
198  \noindent\hbra\\[-.5em] 
199  {\ }\textsc{#1}\\[-.8ex] 
200  \hbox to \textwidth{\leaders\hrule height1.6mm depth-1.5mm\hfill}\\[-.8ex] 
201  }{\\[-.8ex]\hket 
202  \end{tabbing}} 
203 
204 
205\newcommand{\sbline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.2ex}
206\hfill\hspace*{0ex}}} 
207\newcommand{\sline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.1ex}
208\hfill\hspace*{0ex}}} 
209\newcommand{\sentry}[2]{\>$#1$\>\ \smash[t]{\vrule width 0.2mm height
210    1.2\baselineskip depth 1.5\baselineskip}\>#2} 
211 
212\newcommand{\entry}[2]{\>$#1$\>\>#2} 
213\newcommand{\clause}[2]{$#1$\>\>#2} 
214\newcommand{\category}[2]{\clause{#1::=}{#2}} 
215\newcommand{\subclause}[1]{\>\>\>#1} 
216\newcommand{\redrule}[3]{$#1$\>\>$#2$\>\>\>#3} 
217% proofs 
218 
219\newcommand{\Proof}{\noindent {\sc Proof}. } 
220\newcommand{\Proofhint}{\noindent {\sc Proof hint}. } 
221\newcommand{\EndProof}{\qed}
222 
223% figure environment
224 
225\newcommand{\Figbar}{{\center \rule{\hsize}{0.3mm}}}
226 %horizontal thiner line for figures
227\newenvironment{figureplr}[1][t]{\begin{figure}[#1] \Figbar}{\Figbar \end{figure}}
228%environment for figures
229%       ************Macros for mathematical symbols*************
230% Style
231 
232\newcommand{\cl}[1]{{\cal #1}}          % \cl{R} to make R calligraphic
233\newcommand{\la}{\langle}               % the brackets for pairing (see also \pair)
234\newcommand{\ra}{\rangle} 
235 
236\newcommand{\lf}{\lfloor} 
237\newcommand{\rf}{\rfloor} 
238\newcommand{\ul}[1]{\underline{#1}}     % to underline
239\newcommand{\ol}[1]{\overline{#1}}      % to overline
240\newcommand{\ok}{~ok}                   % well formed context
241 
242% Syntax
243 
244\newcommand{\Gives}{\vdash}             % in a type judgment
245\newcommand{\IGives}{\vdash_{I}}        % intuitionistic provability
246\newcommand{\AIGives}{\vdash_{{\it AI}}} %affine-intuitionistic provability
247\newcommand{\CGives}{\vdash_{C}}        % affine-intuitionistic confluent provability
248
249
250\newcommand{\Models}{\mid \! =}              % models
251
252\newcommand{\emptycxt}{\On}              % empty context
253\newcommand{\subs}[2]{[#1 / #2]} 
254\newcommand{\sub}[2]{[#2 / #1]}         % substitution \sub{x}{U} gives [U/x]
255 
256\newcommand{\Sub}[3]{[#3 / #2]#1}       % Substitution with three arguments \Sub{V}{x}{U}
257
258\newcommand{\lsub}[2]{#2 / #1}          % substitution \lsub{x}{U} gives U/x, to  be used in a list.
259 
260\newcommand{\impl}{\supset} 
261\newcommand{\arrow}{\rightarrow}        % right thin arrow
262\newcommand{\trarrow}{\stackrel{*}{\rightarrow}}        % trans closure
263%\newcommand{\limp}{\makebox[5mm]{\,$- \! {\circ}\,$}}   % linear
264                                % implication
265\newcommand{\limp}{\multimap} %linear implication
266\newcommand{\bang}{\, !} 
267% LNCS
268%\newcommand{\bang}{\oc}
269\newcommand{\limpe}[1]{\stackrel{#1}{\multimap}}
270%\newcommand{\hyp}[3]{#1:(#2, #3)}
271\newcommand{\letm}[3]{{\sf let} \ ! #1 = #2 \ {\sf in} \ #3}    % modal let
272\newcommand{\lets}[3]{{\sf let} \ #1 = #2 \ {\sf in} \ #3}    % simple let
273\newcommand{\letp}[3]{{\sf let} \ \S #1 = #2 \ {\sf in} \ #3}    % paragraph let
274\newcommand{\tertype}{{\bf 1}}
275\newcommand{\behtype}{{\bf B}}
276\newcommand{\bt}[1]{{\it BT}(#1)}       % Boehm tree
277\newcommand{\cxt}[1]{#1[~]}             % Context with one hole
278\newcommand{\pr}{\parallel}             % parallel ||
279\newcommand{\Nat}{\mathbf{N}}                 % natural numbers
280\newcommand{\Natmax}{\mathbf{N}_{{\it max}}}  % natural numbers with minus infinity
281\newcommand{\Rat}{\mathbf{Q}^{+}}                 % non-negative rationals
282\newcommand{\Ratmax}{\mathbf{Q}^{+}_{{\it max}}}  % non-negative rationals with minus infinity
283%\newcommand{\Alt}{ \mid\!\!\mid  }
284\newcommand{\isum}{\oplus} 
285\newcommand{\csum}{\uplus}              %context sum
286\newcommand{\dpar}{\mid\!\mid}
287\newcommand{\todo}[1]{}
288                                        % for the production of a grammar containing \mid
289\newcommand{\infer}[2]{\begin{array}{c} #1 \\ \hline #2 \end{array}} 
290                                        % to make a centered inference rule
291 
292% (Meta-)Logic
293 
294\newcommand{\bool}{{\sf bool}}          % boolean values
295\newcommand{\Or}{\vee}                  % disjunction
296\newcommand{\OR}{\bigvee}               % big disjunction
297\newcommand{\AND}{\wedge}               % conjunction
298\newcommand{\ANDD}{\bigwedge}           % big conjunction
299\newcommand{\Arrow}{\Rightarrow}        % right double arrow
300\newcommand{\IFF}{\mbox{~~iff~~}}       % iff in roman and with spaces
301\newcommand{\iffArrow}{\Leftrightarrow} % logical equivalence
302 
303% Semantics
304 
305\newcommand{\dl}{[\![}                  % semantic [[
306\newcommand{\dr}{]\!]}                  % semantic ]]
307
308
309% The equivalences for this paper
310
311% the usual ones
312\newcommand{\ubis}{\approx^u}          % usual labelled weak bis
313\newcommand{\uabis}{\approx^{u}_{ccs}} % usual labelled weak bis on CCS
314
315% the contextual conv sensitive
316\newcommand{\cbis}{\approx}        % convergence sensitive bis
317\newcommand{\cabis}{\approx_{ccs}}  % convergence sensitive bis on CCS
318
319% the labelled conv sensitive
320\newcommand{\lcbis}{\approx^{\ell}} %
321\newcommand{\lcabis}{\approx^{\ell}_{ccs}} % labelled convergence sensitive bis on CCS
322\newcommand{\lcbiswrong}{\approx^{\ell \Downarrow}} %
323
324\newcommand{\maytest}{=_{\Downarrow}}
325\newcommand{\musttest}{=_{\Downarrow_{S}}}
326 
327% Sets
328 
329\newcommand{\prt}[1]{{\cal P}(#1)}      % Parts of a set
330\newcommand{\finprt}[1]{{\cal P}_{fin}(#1)}% Finite parts
331\newcommand{\finprtp}[1]{{\cal P}_{fin}^{+}(#1)}% Non-empty Finite parts
332\newcommand{\union}{\cup}               % union
333\newcommand{\inter}{\cap}               % intersection
334\newcommand{\Union}{\bigcup}            % big union
335\newcommand{\Inter}{\bigcap}            % big intersection
336\newcommand{\cpl}[1]{#1^{c}}            % complement
337\newcommand{\card}{\sharp}              % cardinality
338\newcommand{\minus}{\backslash}         % set difference
339\newcommand{\sequence}[2]{\{#1\}_{#2}}  % ex. \sequence{d_n}{n\in \omega}
340\newcommand{\comp}{\circ}               % functional composition
341%\newcommand{\oset}[1]{\{#1\}}            % set enumeration
342\newcommand{\mset}[1]{\{\! | #1 |\!\}}  % pseudo-set notation {| |}
343 
344% Domains
345 
346\newcommand{\two}{{\bf O}}              % Sierpinski space
347\newcommand{\join}{\vee}                % join
348\newcommand{\JOIN}{\bigvee}             % big join 
349\newcommand{\meet}{\wedge}              % meet
350\newcommand{\MEET}{\bigwedge}           % big meet
351\newcommand{\dcl}{\downarrow}           % down closure
352\newcommand{\ucl}{\uparrow}             % up closure
353\newcommand{\conv}{\downarrow}          % synt. conv. pred. (postfix)
354\newcommand{\diver}{\uparrow}           % diverging term
355\newcommand{\Conv}{\Downarrow}          % sem. conv. pred. (postfix)
356\newcommand{\SConv}{\Downarrow_{S}}          % sem. conv. pred. (postfix)
357\newcommand{\CConv}{\Downarrow_{C}}
358\newcommand{\Diver}{\Uparrow}           % diverging map
359\newcommand{\cpt}[1]{{\cal K}(#1)}      % compacts, write \cpt{D}
360\newcommand{\ret}{\triangleleft}        % retract
361\newcommand{\nor}{\succeq}
362\newcommand{\prj}{\underline{\ret}}     % projection
363\newcommand{\parrow}{\rightharpoonup}   % partial function space
364\newcommand{\ub}[1]{{\it UB}(#1)}       % upper bounds
365\newcommand{\mub}[1]{{\it MUB}(#1)}     % minimal upper bounds
366\newcommand{\lift}[1]{(#1)_{\bot}}      % lifting
367\newcommand{\forget}[1]{\underline{#1}} % forgetful translation
368
369%\newcommand{\rel}[1]{\;{\cal #1}\;}     % infix relation (calligraphic)
370\newcommand{\rl}[1]{\;{\cal #1}\;}             % infix relation
371\newcommand{\rel}[1]{{\cal #1}}         %calligraphic relation with no
372                                        %extra space
373\newcommand{\per}[1]{\;#1 \;} 
374\newcommand{\wddagger}{\natural}  % weak suspension
375%\newcommand{\wddagger}{=\!\!\!\!\parallel}  % weak suspension
376% Categories
377 
378\newcommand{\pair}[2]{\langle #1 , #2 \rangle} % pairing \pair{x}{y}, do not use < >.
379 
380%               *******  Notation for the $\pi$-calculus *********
381% Syntax:
382 
383\newcommand{\fn}[1]{{\it fn}(#1)}                       % free names
384\newcommand{\bn}[1]{{\it bn}(#1)}                       % bound names
385\newcommand{\names}[1]{{\it n}(#1)}                     % names
386\newcommand{\true}{{\sf t}}                             % true
387\newcommand{\false}{{\sf f}}                            % false
388\newcommand{\pio}{\pi_1}                                % 1 receptor calculus
389\newcommand{\pioo}{\pi_{1}^{r}} 
390\newcommand{\piom}{\pi_{1}^{-}}                         % 1 receptor calculus wo match
391\newcommand{\pioi}{\pi_{1I}}                    % 1 receptor I-calculus
392\newcommand{\pifo}{\pi_{\w{1f}}}                                % functional calculus
393\newcommand{\pilo}{\pi_{\w{1l}}}                                % located calculus
394\newcommand{\sort}[1]{{\it st}(#1)}                     % sort
395\newcommand{\ia}[1]{{\it ia}(#1)}                     % sort
396\newcommand{\ite}[3]{{\sf if~} #1 {\sf ~then~} #2 {\sf ~else~} #3}      %if then else
397\newcommand{\casep}[2]{{\sf case}^{\times}(#1, \pair{x}{y}\Arrow#2)}      %case on pairs
398\newcommand{\casel}[3]{{\sf case}^{L}(#1, #2, \s{cons}(x,y)\Arrow#3)}      %case on lists
399\newcommand{\caseb}[3]{{\sf case}^{b}(#1, #2, \s{cons}(x,y)\Arrow#3)}      %case on lists
400\newcommand{\nil}{{\sf nil}} 
401\newcommand{\cons}{{\sf cons}} 
402\newcommand{\idle}[1]{{\it Idle}(#1)}                   %idle process
403\newcommand{\conf}[1]{\{ #1 \}}                         %configuration
404\newcommand{\link}[2]{#1 \mapsto #2}                    %likn a ->b
405\newcommand{\mand}{\mbox{ and }} 
406\newcommand{\dvec}[1]{\tilde{{\bf #1}}}                 %double vector
407\newcommand{\erloc}[1]{{\it er}_{l}(#1)}                % location erasure
408\newcommand{\w}[1]{{\it #1}}    %To write in math style
409\newcommand{\vcb}[1]{{\bf #1}} 
410\newcommand{\lc}{\langle\!|} 
411\newcommand{\rc}{|\!\rangle} 
412\newcommand{\obj}[1]{{\it obj}(#1)} 
413\newcommand{\move}[1]{{\sf move}(#1)} 
414\newcommand{\qqs}[2]{\forall\, #1\;\: #2} 
415\newcommand{\qtype}[4]{\forall #1 :  #2 . (#4,#3)} 
416\newcommand{\xst}[2]{\exists\, #1\;\: #2} 
417\newcommand{\xstu}[2]{\exists\, ! #1\;\: #2} 
418\newcommand{\dpt}{\,:\,} 
419\newcommand{\cond}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3} 
420\newcommand{\s}[1]{{\sf #1}}    % sans-serif 
421\newcommand{\vc}[1]{{\bf #1}} 
422\newcommand{\lnorm}{\lbrack\!\lbrack} 
423\newcommand{\rnorm}{\rbrack\!\rbrack} 
424\newcommand{\sem}[1]{\underline{#1}} 
425\newcommand{\tra}[1]{\langle #1 \rangle}
426\newcommand{\trb}[1]{[ #1 ]}
427\newcommand{\squn}{\mathop{\scriptstyle\sqcup}} 
428\newcommand{\lcro}{\langle\!|} 
429\newcommand{\rcro}{|\!\rangle} 
430\newcommand{\semi}[1]{\lcro #1\rcro} 
431\newcommand{\sell}{\,\ell\,} 
432\newcommand{\SDZ}[1]{\marginpar{\textbf{SDZ:} {#1}}} 
433 
434\newcommand{\when}[3]{{\sf when}~#1~{\sf then}~#2~{\sf else}~#3} 
435\newcommand{\wthen}[2]{{\sf when}~#1~{\sf then}~#2~} 
436\newcommand{\welse}[1]{{\sf else}~#1} 
437
438%Pour la fleche double, il faut rajouter :
439%      \usepackage{mathtools}
440
441\newcommand{\act}[1]{\xrightarrow{#1}} %labelled actionlow %high
442
443\newcommand{\lact}[1]{\stackrel{#1}{\makebox[5mm]{\,$- \! {\circ}\,$}}}
444
445\newcommand{\set}[1]{\{#1\}}
446\newcommand{\pst}[2]{{\sf pset}(#1,#2)}
447\newcommand{\st}[2]{{\sf set}(#1,#2)}
448\newcommand{\wrt}[2]{{\sf w}(#1,#2)}
449
450\newcommand{\chtype}[2]{{\it Ch_{#1}(#2)}}
451\newcommand{\rgtype}[2]{{\it {\sf Reg}_{#1} #2}}
452
453\newcommand{\get}[1]{{\sf get}(#1)}
454
455%\newcommand{\wact}[1]{\xRightarrow{#1}} %weak labelled action low high
456
457%\newcommand{\mact}[1]{\xrightarrow{#1}_{m}} %labelled action low %high
458
459%\newcommand{\wmact}[1]{\xRightarrow{#1}_{m}} %weak labelled action low high
460
461%\newcommand{\act}[1]{\stackrel{#1}{\rightarrow}} %labelled action low
462                                %%%high
463
464\newcommand{\acteq}[1]{\stackrel{#1}{\leadsto}} %labelled action low
465                                %%%high
466
467
468%\newcommand{\actI}[1]{\stackrel{#1}{\rightarrow_{1}}} %labelled action low
469\newcommand{\actI}[1]{\xrightarrow{#1}_{1}}
470
471%\newcommand{\actII}[1]{\stackrel{#1}{\rightarrow_{2}}} %labelled action low
472\newcommand{\actII}[1]{\xrightarrow{#1}_{2}}
473
474
475 \newcommand{\wact}[1]{\stackrel{#1}{\Rightarrow}} %weak labelled action low high
476\newcommand{\wactI}[1]{\stackrel{#1}{\Rightarrow_{1}}} %weak labelled action low high
477\newcommand{\wactII}[1]{\stackrel{#1}{\Rightarrow_{2}}} %weak labelled action low high
478
479
480\newcommand{\mact}[1]{\stackrel{#1}{\rightarrow_{m}}} %labelled action low
481%high
482\newcommand{\wmact}[1]{\stackrel{#1}{\Rightarrow_{m}}} %weak labelled action low high
483 
484%\newcommand{\lact}[1]{\stackrel{#1}{\leftarrow}}
485\newcommand{\lwact}[1]{\stackrel{#1}{\Leftarrow}} 
486 
487 
488 
489\newcommand{\eval}{\Downarrow} 
490\newcommand{\Eval}[1]{\Downarrow^{#1}} 
491 
492 
493\newcommand{\Z}{{\bf Z}} 
494\newcommand{\Real}{\mathbb{R}^{+}} 
495\newcommand{\Return}{\ensuremath{\mathtt{return}}\xspace}                 
496\newcommand{\Stop}{\ensuremath{\mathtt{stop}}\xspace} 
497\newcommand{\Wait}{\ensuremath{\mathtt{wait}}\xspace} 
498\newcommand{\Read}{\ensuremath{\mathtt{read}}\xspace} 
499\newcommand{\Write}{\ensuremath{\mathtt{write}}\xspace} 
500\newcommand{\Yield}{\ensuremath{\mathtt{yield}}\xspace} 
501\newcommand{\Next}{\ensuremath{\mathtt{next}}\xspace} 
502\newcommand{\Load}{\ensuremath{\mathtt{load}}\xspace} 
503\newcommand{\Call}{\ensuremath{\mathtt{call}}\xspace} 
504\newcommand{\Tcall}{\ensuremath{\mathtt{tcall}}\xspace} 
505\newcommand{\Pop}{\ensuremath{\mathtt{pop}}\xspace} 
506\newcommand{\Build}{\ensuremath{\mathtt{build}}\xspace} 
507\newcommand{\Branch}{\ensuremath{\mathtt{branch}}\xspace} 
508\newcommand{\Goto}{\ensuremath{\mathtt{goto}}\xspace} 
509 
510\newcommand{\hatt}[1]{#1^{+}} 
511\newcommand{\Of}{\mathbin{\w{of}}} 
512 
513\newcommand{\susp}{\downarrow} 
514\newcommand{\lsusp}{\Downarrow_L} 
515\newcommand{\wsusp}{\Downarrow} 
516\newcommand{\commits}{\searrow} 
517 
518 
519\newcommand{\spi}{S\pi} 
520 
521
522 \newcommand{\pres}[2]{#1\triangleright #2} %TCCS else next (alternative)
523% \newcommand{\pres}[2]{ \lfloor #1 \rfloor (#2)}  %TCCS else next
524\newcommand{\present}[3]{{\sf present} \ #1 \ {\sf do } \ #2 \ {\sf  else} \ #3}
525
526
527\newcommand{\tick}{{\sf tick}}          %tick action
528
529 
530 
531\newcommand{\sbis}{\equiv_L} 
532\newcommand{\emit}[2]{\ol{#1}#2} 
533%\newcommand{\present}[4]{#1(#2).#3,#4}
534\newcommand{\match}[4]{[#1=#2]#3,#4}       %pi-equality
535
536\newcommand{\matchv}[4]{[#1 \unrhd #2]#3,#4}
537
538\newcommand{\new}[2]{\nu #1 \ #2} 
539\newcommand{\outact}[3]{\new{{\bf #1}}{\emit{#2}{#3}}} 
540\newcommand{\real}{\makebox[5mm]{\,$\|\!-$}}% realizability relation
541
542\newcommand{\regterm}[2]{{\sf reg}_{#1} #2}
543\newcommand{\thread}[1]{{\sf thread} \ #1}
544\newcommand{\store}[2]{(#1 \leftarrow #2)}
545\newcommand{\pstore}[2]{(#1 \Leftarrow #2)}
546
547\newcommand{\regtype}[2]{{\sf Reg}_{#1} #2}
548\newcommand{\uregtype}[3]{{\sf Reg}_{#1}(#2, #3)}
549\newcommand{\urtype}[2]{{\sf Reg}(#1, #2)}
550
551\newcommand{\upair}[2]{[#1,#2]}
552\newcommand{\letb}[3]{\mathsf{let}\;\oc #1 = #2\;\mathsf{in}\;#3}
553
554\newcommand{\vlt}[1]{{\cal V}(#1)}
555\newcommand{\prs}[1]{{\cal P}(#1)}
556
557\newcommand{\imp}{{\sf Imp}}            %imp language
558\newcommand{\vm}{{\sf Vm}}              %virtual machine language
559\newcommand{\mips}{{\sf Mips}}          %Mips language
560\newcommand{\C}{{\sf C}}                % C language
561\newcommand{\Clight}{{\sf Clight}}        %C light language
562\newcommand{\Cminor}{{\sf Cminor}}
563\newcommand{\RTLAbs}{{\sf RTLAbs}}
564\newcommand{\RTL}{{\sf RTL}}
565\newcommand{\ERTL}{{\sf ERTL}}
566\newcommand{\LTL}{{\sf LTL}}
567\newcommand{\LIN}{{\sf LIN}}
568\newcommand{\access}[1]{\stackrel{#1}{\leadsto}}
569
570\newcommand{\codeex}[1]{\texttt{#1}}   % code example
571
572\title{CerCo: Certified Complexity\thanks{The project CerCo acknowledges the
573financial support of the Future and Emerging Technologies (FET) programme within
574the Seventh Framework Programme for Research of the European Commission, under
575FET-Open grant number: 243881}}
576\subtitle{Source-level complexity analysis for a large fragment of C}
577\journalname{Journal of Automated Reasoning}
578\titlerunning{Certified Complexity}
579\date{Received: date / Accepted: date}
580\author{Jaap Boender \and Brian Campbell \and Dominic P. Mulligan \and Claudio Sacerdoti~Coen
581        \and %Roberto
582Roberto~M. Amadio \and
583Nicolas Ayache \and
584Fran\c{c}ois Bobot \and
585Ilias Garnier \and
586Antoine Madet \and
587James McKinna \and
588Mauro Piccolo \and
589Randy Pollack \and
590Yann R\'{e}gis-Gianas \and
591Ian Stark \and
592Paolo Tranquilli} % who else?
593\authorrunning{Boender, Campbell, Mulligan, and Sacerdoti~Coen}
594\institute{Roberto M. Amadio, Antoine Madet, and Yann R\'{e}gis-Gianas \at
595            Universit\'e Paris Diderot (Paris 7), Paris, France.
596           \and
597           Nicolas Ayache \at
598            IKOS Consulting, France.
599           \and
600           Fran\c{c}ois Bobot \at
601           Software Reliability Laboratory, CEA, France.
602           \and
603           Jaap Boender \at
604              Middlesex University London, United Kingdom.
605           \and
606           Brian Campbell, James McKinna, Randy Pollack, and Ian Stark \at
607              University of Edinburgh, United Kingdom.
608           \and
609           Ilias Garnier, \at
610             \'Ecole Normale Sup\'erieure, Paris, France.
611           \and
612           Dominic P. Mulligan \at
613             University of Cambridge, United Kingdom.
614           \and
615           Claudio Sacerdoti~Coen \at
616              University of Bologna, Italy.}
617
618\begin{document}
619
620\maketitle
621
622\begin{abstract}
623Concrete non-functional properties of programs---for example, time and space usage as measured in basal units of measure such as milliseconds and bytes allocated---are important components of the specification of a program, and therefore overall program correctness.
624Indeed, for many application domains, concrete complexity analysis is arguably more important than any asymptotic complexity analysis.
625Libraries exporting cryptographic primitives that must be impervious to timing side-channel attacks, or real-time applications with hard timing limits on responsiveness, are examples.
626
627Worst Case Execution Time tools, based on abstract interpretation, currently represent the state-of-the-art in determining concrete time bounds for a program execution.
628These tools suffer from a number of disadvantages, not least the fact that all analysis is performed on machine code, rather than high-level source code, making results hard to interpret by programmers.
629Further, these tools are often complex pieces of software, whose analysis is hard to trust.
630More ideal would be a mechanism to `lift' a cost model from the machine code generated by a compiler, back to the source code level, where analyses could be performed in terms understood by the programmer.
631How one could incorporate the precision of traditional static analyses into such a high-level approach---and how this could be done reliably---is not \emph{a priori} clear.
632
633In this paper, we describe the scientific contributions of the European Union's FET-Open Project CerCo (`Certified Complexity').
634CerCo's main achievement is the development of a technique for analysing non-functional properties of programs at the source level, with little or no loss of accuracy, and a small trusted code base.
635The core component of the project is a compiler for a large fragment of the C programming language, verified in the Matita theorem prover, that produces an instrumented copy of the source code in addition to generating object code.
636This instrumentation exposes, and tracks precisely, the concrete (non-asymptotic) computational cost of the input program at the source level.
637Untrusted invariant generators and trusted theorem provers may then be used to compute and certify the parametric execution time of the code.
638
639We describe the architecture of our C compiler, its proof of correctness, and the associated toolchain developed around the compiler.
640Using our toolchain, we describe a case study in applying our technique to the verification of concrete timing bounds for cryptographic code.
641
642\keywords{Verified compilation \and Complexity analysis \and Worst Case Execution Time analysis \and CerCo (`Certified Complexity') \and Matita}
643\end{abstract}
644
645\include{introduction}
646\include{architecture}
647\include{specification}
648\include{proof}
649\include{development}
650\include{framac}
651\include{conclusions}
652
653\begin{acknowledgements}
654\end{acknowledgements}
655
656\bibliographystyle{spmpsci}
657\bibliography{cerco}
658
659\end{document}
Note: See TracBrowser for help on using the repository browser.