Changeset 3420 for Papers/fopara2013


Ignore:
Timestamp:
Feb 10, 2014, 5:18:47 PM (6 years ago)
Author:
campbell
Message:

Parametric example for FOPARA.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3419 r3420  
    2525%\def\lstlanguagefiles{lst-grafite.tex}
    2626%\lstset{language=Grafite}
    27 \lstset{language=C}
     27\lstset{language=C,basewidth=.5em,lineskip=-2pt}
    2828
    2929\newlength{\mylength}
     
    351351\begin{tabular}{l@{\hspace{0.2cm}}|@{\hspace{0.2cm}}l}
    352352\begin{lstlisting}
    353 char a[] = {3, 2, 7, -4};
    354 char treshold = 4;
     353char a[] = {3, 2, 7, 14};
     354char threshold = 4;
     355
     356int count(char *p, int len) {
     357  char j;
     358  int found = 0;
     359  for (j=0; j < len; j++) {
     360    if (*p <= threshold)
     361      found++;
     362    p++;
     363    }
     364  return found;
     365}
    355366
    356367int main() {
    357   char j;
    358   char *p = a;
    359   int found = 0;
    360   for (j=0; j < 4; j++) {
    361     if (*p <= treshold)
    362       { found++; }
    363     p++;
    364   }
    365   return found;
     368  return count(a,4);
    366369}
    367370\end{lstlisting}
     
    389392\draw [->] (cerco) -- (cost);
    390393\draw [->] ([yshift=1ex]cerco.south west) coordinate (t) --
    391     node {C source+cost annotations}
     394    node {C source+\color{red}{cost annotations}}
    392395    (t-|left) coordinate (cerco out);
    393396\draw [->] ([yshift=1ex]cost.south west) coordinate (t) --
    394     node {C source+cost annotations\\+synthesized assertions}
     397    node {C source+\color{red}{cost annotations}\\+\color{blue}{synthesized assertions}}
    395398    (t-|left) coordinate (out);
    396399{[densely dashed]
    397400\draw [<-] ([yshift=-1ex]ded.north west) coordinate (t) --
    398     node {C source+cost annotations\\+complexity assertions}
     401    node {C source+\color{red}{cost annotations}\\+\color{blue}{complexity assertions}}
    399402    (t-|left) coordinate (ded in) .. controls +(-.5, 0) and +(-.5, 0) .. (out);
    400403\draw [->] ([yshift=1ex]ded.south west) coordinate (t) --
     
    422425\end{tabular}
    423426\caption{On the left: code to count the array's elements
    424  that are less than or equal to the treshold. On the right: CerCo's interaction
     427 that are less than or equal to the threshold. On the right: CerCo's interaction
    425428 diagram. CerCo's components are drawn solid.}
    426429\label{test1}
     
    439442assertions, a general purpose deductive platform produces proof obligations
    440443which in turn can be closed by automatic or interactive provers, ending in a
    441 proof certificate. Nine proof obligations are generated
    442 from~\autoref{itest1} (to prove that the loop invariant holds after
    443 one execution if it holds before, to prove that the whole program execution
    444 takes at most 1228 cycles, etc.). The CVC3 prover closes all obligations
    445 in a few seconds on routine commodity hardware.
     444proof certificate.
     445
     446% NB: if you try this example with the live CD you should increase the timeout
     447
     448Twelve proof obligations are generated from~\autoref{itest1} (to prove
     449that the loop invariant holds after one execution if it holds before,
     450to prove that the whole program execution takes at most 1358 cycles,
     451etc.).  Note that the synthesised time bound for \lstinline'count',
     452$178+214*(1+\lstinline'len')$ cycles, is parametric in the length of
     453the array. The CVC3 prover
     454closes all obligations within half a minute on routine commodity
     455hardware.  A simpler non-parametric version can be solved in a few
     456seconds.
    446457%
    447458\fvset{commandchars=\\\{\}}
     
    451462\begin{figure}[!p]
    452463\begin{lstlisting}
    453 |int __cost = 33; int __stack = 5, __stack_max = 5;|
    454 |void __cost_incr(int incr) { __cost = __cost + incr; }|
     464|int __cost = 33, __stack = 5, __stack_max = 5;|
     465|void __cost_incr(int incr) { __cost += incr; }|
    455466|void __stack_incr(int incr) {
    456   __stack = __stack + incr;
     467  __stack += incr;
    457468  __stack_max = __stack_max < __stack ? __stack : __stack_max;
    458469}|
    459470
    460 char a[4] = { 3, 2, 7, 252, };
    461 char treshold = 4;
    462 
    463 /*@ behaviour stack_cost:
    464       ensures __stack_max <=
    465               __max(\old(__stack_max), \old(__stack));
     471char a[4] = {3, 2, 7, 14};  char threshold = 4;
     472
     473/*@ behavior stack_cost:
     474      ensures __stack_max <= __max(\old(__stack_max), 4+\old(__stack));
    466475      ensures __stack == \old(__stack);
    467      
    468     behaviour time_cost:
    469       ensures __cost <= \old(__cost)+1228; */
    470 int main(void)
    471 {
    472   char j;
    473   char *p;
    474   int found;
    475   |__stack_incr(0); __cost_incr(91);|
    476   p = a;
    477   found = 0;
     476    behavior time_cost:
     477      ensures __cost <= \old(__cost)+(178+214*__max(1+\at(len,Pre), 0));
     478*/
     479int count(unsigned char *p, int len) {
     480  char j;  int found = 0;
     481  |__stack_incr(4);  __cost_incr(111);|
    478482  $__l: /* internal */$
    479483  /*@ for time_cost: loop invariant
    480         __cost <=
    481         \at(__cost,__l)+220*(__max(\at(5-j,__l), 0)
    482                        -__max (5-j, 0));
     484        __cost <= \at(__cost,__l)+
     485                  214*(__max(\at((len-j)+1,__l), 0)-__max(1+(len-j), 0));
    483486      for stack_cost: loop invariant
    484487        __stack_max == \at(__stack_max,__l);
    485488      for stack_cost: loop invariant
    486489        __stack == \at(__stack,__l);
    487       loop variant 4-j; */
    488   for (j = 0; j < 4; j++) {
    489     |__cost_incr(76);|
    490     if (*p <= treshold) {
    491       |__cost_incr(144);|
    492       found++;
    493     } else {
    494       |__cost_incr(122);|
    495     }
    496     p++;
     490      loop variant len-j;
     491  */
     492  for (j = 0; j < len; j++) {
     493    |__cost_incr(78);|
     494    if (*p <= threshold) { |__cost_incr(136);| found ++; }
     495    else { |__cost_incr(114);| }
     496    p ++;
    497497  }
    498   |__cost_incr(37); __stack_incr(-0);|
     498  |__cost_incr(67);  __stack_incr(-4);|
    499499  return found;
     500}
     501
     502/*@ behavior stack_cost:
     503      ensures __stack_max <= __max(\old(__stack_max), 6+\old(__stack));
     504      ensures __stack == \old(__stack);
     505    behavior time_cost:
     506      ensures __cost <= \old(__cost)+1358;
     507*/
     508int main(void) {
     509  int t;
     510  |__stack_incr(2);  __cost_incr(110);|
     511  t = count(a,4);
     512  |__stack_incr(-2);|
     513  return t;
    500514}
    501515\end{lstlisting}
Note: See TracChangeset for help on using the changeset viewer.