Changeset 3420 for Papers/fopara2013/fopara13.tex

Timestamp:

Feb 10, 2014, 5:18:47 PM (7 years ago)

Author:

campbell

Message:

Parametric example for FOPARA.

File:

• Papers/fopara2013/fopara13.tex (modified) (6 diffs)

Papers/fopara2013/fopara13.tex

@@ -25 +25 @@
 %\def\lstlanguagefiles{lst-grafite.tex}
 %\lstset{language=Grafite}
-\lstset{language=C}
+\lstset{language=C,basewidth=.5em,lineskip=-2pt}
 
 \newlength{\mylength}
@@ -351 +351 @@
 \begin{tabular}{l@{\hspace{0.2cm}}|@{\hspace{0.2cm}}l}
 \begin{lstlisting}
-char a[] = {3, 2, 7, -4};
-char treshold = 4;
+char a[] = {3, 2, 7, 14};
+char threshold = 4;
+
+int count(char *p, int len) {
+  char j;
+  int found = 0;
+  for (j=0; j < len; j++) {
+    if (*p <= threshold)
+      found++;
+    p++;
+    }
+  return found;
+}
 
 int main() {
-  char j;
-  char *p = a;
-  int found = 0;
-  for (j=0; j < 4; j++) {
-    if (*p <= treshold)
-      { found++; }
-    p++;
-  }
-  return found;
+  return count(a,4);
 }
 \end{lstlisting}
@@ -389 +392 @@
 \draw [->] (cerco) -- (cost);
 \draw [->] ([yshift=1ex]cerco.south west) coordinate (t) --
-    node {C source+cost annotations}
+    node {C source+\color{red}{cost annotations}}
     (t-|left) coordinate (cerco out);
 \draw [->] ([yshift=1ex]cost.south west) coordinate (t) --
-    node {C source+cost annotations\\+synthesized assertions}
+    node {C source+\color{red}{cost annotations}\\+\color{blue}{synthesized assertions}}
     (t-|left) coordinate (out);
 {[densely dashed]
 \draw [<-] ([yshift=-1ex]ded.north west) coordinate (t) --
-    node {C source+cost annotations\\+complexity assertions}
+    node {C source+\color{red}{cost annotations}\\+\color{blue}{complexity assertions}}
     (t-|left) coordinate (ded in) .. controls +(-.5, 0) and +(-.5, 0) .. (out);
 \draw [->] ([yshift=1ex]ded.south west) coordinate (t) --
@@ -422 +425 @@
 \end{tabular}
 \caption{On the left: code to count the array's elements
- that are less than or equal to the treshold. On the right: CerCo's interaction
+ that are less than or equal to the threshold. On the right: CerCo's interaction
  diagram. CerCo's components are drawn solid.}
 \label{test1}
@@ -439 +442 @@
 assertions, a general purpose deductive platform produces proof obligations 
 which in turn can be closed by automatic or interactive provers, ending in a 
-proof certificate. Nine proof obligations are generated
-from~\autoref{itest1} (to prove that the loop invariant holds after
-one execution if it holds before, to prove that the whole program execution
-takes at most 1228 cycles, etc.). The CVC3 prover closes all obligations
-in a few seconds on routine commodity hardware.
+proof certificate.
+
+% NB: if you try this example with the live CD you should increase the timeout
+
+Twelve proof obligations are generated from~\autoref{itest1} (to prove
+that the loop invariant holds after one execution if it holds before,
+to prove that the whole program execution takes at most 1358 cycles,
+etc.).  Note that the synthesised time bound for \lstinline'count',
+$178+214*(1+\lstinline'len')$ cycles, is parametric in the length of
+the array. The CVC3 prover
+closes all obligations within half a minute on routine commodity
+hardware.  A simpler non-parametric version can be solved in a few
+seconds.
 %
 \fvset{commandchars=\\\{\}}
@@ -451 +462 @@
 \begin{figure}[!p]
 \begin{lstlisting}
-|int __cost = 33; int __stack = 5, __stack_max = 5;|
-|void __cost_incr(int incr) { __cost = __cost + incr; }|
+|int __cost = 33, __stack = 5, __stack_max = 5;|
+|void __cost_incr(int incr) { __cost += incr; }|
 |void __stack_incr(int incr) {
-  __stack = __stack + incr;
+  __stack += incr;
   __stack_max = __stack_max < __stack ? __stack : __stack_max;
 }|
 
-char a[4] = { 3, 2, 7, 252, };
-char treshold = 4;
-
-/*@ behaviour stack_cost:
-      ensures __stack_max <=
-              __max(\old(__stack_max), \old(__stack));
+char a[4] = {3, 2, 7, 14};  char threshold = 4;
+
+/*@ behavior stack_cost:
+      ensures __stack_max <= __max(\old(__stack_max), 4+\old(__stack));
       ensures __stack == \old(__stack);
-      
-    behaviour time_cost:
-      ensures __cost <= \old(__cost)+1228; */
-int main(void)
-{
-  char j;
-  char *p;
-  int found;
-  |__stack_incr(0); __cost_incr(91);|
-  p = a;
-  found = 0;
+    behavior time_cost:
+      ensures __cost <= \old(__cost)+(178+214*__max(1+\at(len,Pre), 0));
+*/
+int count(unsigned char *p, int len) {
+  char j;  int found = 0;
+  |__stack_incr(4);  __cost_incr(111);|
   $__l: /* internal */$
   /*@ for time_cost: loop invariant
-        __cost <=
-        \at(__cost,__l)+220*(__max(\at(5-j,__l), 0)
-                       -__max (5-j, 0));
+        __cost <= \at(__cost,__l)+
+                  214*(__max(\at((len-j)+1,__l), 0)-__max(1+(len-j), 0));
       for stack_cost: loop invariant
         __stack_max == \at(__stack_max,__l);
       for stack_cost: loop invariant
         __stack == \at(__stack,__l);
-      loop variant 4-j; */
-  for (j = 0; j < 4; j++) {
-    |__cost_incr(76);|
-    if (*p <= treshold) {
-      |__cost_incr(144);|
-      found++;
-    } else {
-      |__cost_incr(122);|
-    }
-    p++;
+      loop variant len-j;
+  */
+  for (j = 0; j < len; j++) {
+    |__cost_incr(78);|
+    if (*p <= threshold) { |__cost_incr(136);| found ++; }
+    else { |__cost_incr(114);| }
+    p ++;
   }
-  |__cost_incr(37); __stack_incr(-0);|
+  |__cost_incr(67);  __stack_incr(-4);|
   return found;
+}
+
+/*@ behavior stack_cost:
+      ensures __stack_max <= __max(\old(__stack_max), 6+\old(__stack));
+      ensures __stack == \old(__stack);
+    behavior time_cost:
+      ensures __cost <= \old(__cost)+1358;
+*/
+int main(void) {
+  int t;
+  |__stack_incr(2);  __cost_incr(110);|
+  t = count(a,4);
+  |__stack_incr(-2);|
+  return t;
 }
 \end{lstlisting}