Changeset 3310


Ignore:
Timestamp:
Jun 4, 2013, 6:19:47 PM (4 years ago)
Author:
sacerdot
Message:

An example.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3309 r3310  
    77\usepackage{color}
    88\usepackage{fancybox}
     9\usepackage{fancyvrb}
    910\usepackage{graphicx}
    1011\usepackage[colorlinks]{hyperref}
     
    2021%\def\lstlanguagefiles{lst-grafite.tex}
    2122%\lstset{language=Grafite}
     23\lstset{language=C}
    2224
    2325\newlength{\mylength}
     
    234236I/O operations can be performed in the prefix of the run, but not in the measurable sub-run. Therefore we prove that we can predict reaction times, but not I/O times, as it should be.
    235237
     238\begin{figure}[t]
     239\begin{lstlisting}
     240char a[] = {3, 2, 7, -4};
     241char treshold = 4;
     242
     243int main() {
     244        char j;
     245        char *p = a;
     246        int found = 0;
     247        for (j=0; j < 4; j++) {
     248                if (*p <= treshold) { found++; }
     249                p++;
     250        }
     251        return found;
     252}
     253\end{lstlisting}
     254\caption{A simple C program.}
     255\label{test1}
     256\end{figure}
     257
     258\fvset{commandchars=\\\{\}}
     259
     260\lstset{morecomment=[s][\color{blue}]{/*@}{*/},
     261        moredelim=[is][\color{blue}]{$}{$},
     262        moredelim=[is][\color{red}]{|}{|}}
     263
     264
     265\begin{figure}[!p]
     266\begin{lstlisting}
     267|int __cost = 33; int __stack = 5, __stack_max = 5;|
     268
     269|void __cost_incr(int incr) { __cost = __cost + incr; }|
     270
     271|void __stack_incr(int incr) {
     272  __stack = __stack + incr;
     273  __stack_max = __stack_max < __stack ? __stack : __stack_max;
     274}|
     275
     276unsigned char a[4] = { 3, 2, 7, 252, };
     277unsigned char treshold = 4;
     278
     279/*@ behavior stack_cost:
     280      ensures __stack_max <=
     281              __max(\old(__stack_max), \old(__stack));
     282      ensures __stack == \old(__stack);
     283     
     284    behavior time_cost:
     285      ensures __cost <= \old(__cost)+1228; */
     286int main(void)
     287{
     288  char j;
     289  char *p;
     290  int found;
     291  |__stack_incr(0); __cost_incr(91);|
     292  p = a;
     293  found = 0;
     294  $__l: /* internal */$
     295  /*@ for time_cost: loop invariant
     296        __cost <=
     297        \at(__cost,__l)+220*(__max(\at(5-j,__l), 0)-__max (5-j, 0));
     298      for stack_cost: loop invariant
     299        __stack_max == \at(__stack_max,__l);
     300      for stack_cost: loop invariant
     301        __stack == \at(__stack,__l);
     302      loop variant 4-j; */
     303  for (j = 0; j < 4; j++) {
     304    |__cost_incr(76);|
     305    if (*p <= treshold) {
     306      |__cost_incr(144);|
     307      found++;
     308    } else {
     309      |__cost_incr(122);|
     310    }
     311    p++;
     312  }
     313  |__cost_incr(37); __stack_incr(-0);|
     314  return found;
     315}
     316\end{lstlisting}
     317\caption{The instrumented version of the program in \autoref{test1}.}
     318\label{itest1}
     319\end{figure}
     320
     321
    236322\bibliography{fopara13.bib}
    237323
Note: See TracChangeset for help on using the changeset viewer.