Changeset 3420
 Timestamp:
 Feb 10, 2014, 5:18:47 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/fopara2013/fopara13.tex
r3419 r3420 25 25 %\def\lstlanguagefiles{lstgrafite.tex} 26 26 %\lstset{language=Grafite} 27 \lstset{language=C }27 \lstset{language=C,basewidth=.5em,lineskip=2pt} 28 28 29 29 \newlength{\mylength} … … 351 351 \begin{tabular}{l@{\hspace{0.2cm}}@{\hspace{0.2cm}}l} 352 352 \begin{lstlisting} 353 char a[] = {3, 2, 7, 4}; 354 char treshold = 4; 353 char a[] = {3, 2, 7, 14}; 354 char threshold = 4; 355 356 int 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 } 355 366 356 367 int 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); 366 369 } 367 370 \end{lstlisting} … … 389 392 \draw [>] (cerco)  (cost); 390 393 \draw [>] ([yshift=1ex]cerco.south west) coordinate (t)  391 node {C source+ cost annotations}394 node {C source+\color{red}{cost annotations}} 392 395 (tleft) coordinate (cerco out); 393 396 \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}} 395 398 (tleft) coordinate (out); 396 399 {[densely dashed] 397 400 \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}} 399 402 (tleft) coordinate (ded in) .. controls +(.5, 0) and +(.5, 0) .. (out); 400 403 \draw [>] ([yshift=1ex]ded.south west) coordinate (t)  … … 422 425 \end{tabular} 423 426 \caption{On the left: code to count the array's elements 424 that are less than or equal to the t reshold. On the right: CerCo's interaction427 that are less than or equal to the threshold. On the right: CerCo's interaction 425 428 diagram. CerCo's components are drawn solid.} 426 429 \label{test1} … … 439 442 assertions, a general purpose deductive platform produces proof obligations 440 443 which 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. 444 proof certificate. 445 446 % NB: if you try this example with the live CD you should increase the timeout 447 448 Twelve proof obligations are generated from~\autoref{itest1} (to prove 449 that the loop invariant holds after one execution if it holds before, 450 to prove that the whole program execution takes at most 1358 cycles, 451 etc.). Note that the synthesised time bound for \lstinline'count', 452 $178+214*(1+\lstinline'len')$ cycles, is parametric in the length of 453 the array. The CVC3 prover 454 closes all obligations within half a minute on routine commodity 455 hardware. A simpler nonparametric version can be solved in a few 456 seconds. 446 457 % 447 458 \fvset{commandchars=\\\{\}} … … 451 462 \begin{figure}[!p] 452 463 \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; } 455 466 void __stack_incr(int incr) { 456 __stack = __stack +incr;467 __stack += incr; 457 468 __stack_max = __stack_max < __stack ? __stack : __stack_max; 458 469 } 459 470 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)); 471 char 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)); 466 475 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 */ 479 int count(unsigned char *p, int len) { 480 char j; int found = 0; 481 __stack_incr(4); __cost_incr(111); 478 482 $__l: /* internal */$ 479 483 /*@ for time_cost: loop invariant 480 __cost <= 481 \at(__cost,__l)+220*(__max(\at(5j,__l), 0) 482 __max (5j, 0)); 484 __cost <= \at(__cost,__l)+ 485 214*(__max(\at((lenj)+1,__l), 0)__max(1+(lenj), 0)); 483 486 for stack_cost: loop invariant 484 487 __stack_max == \at(__stack_max,__l); 485 488 for stack_cost: loop invariant 486 489 __stack == \at(__stack,__l); 487 loop variant 4j; */ 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 lenj; 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 ++; 497 497 } 498 __cost_incr( 37); __stack_incr(0);498 __cost_incr(67); __stack_incr(4); 499 499 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 */ 508 int main(void) { 509 int t; 510 __stack_incr(2); __cost_incr(110); 511 t = count(a,4); 512 __stack_incr(2); 513 return t; 500 514 } 501 515 \end{lstlisting}
Note: See TracChangeset
for help on using the changeset viewer.