Wiki

Programs consisting of nonlinear invariants that can express runtime complexities.

fig1a (Gulwani CAV '09)

#!c
void fig1a(int m){
     int x = 0;
     int y = 0;
     int t = 0;
     while(x < 100){
      if (y < m){
           y++;
      }
      else{        
           x++;
      }
      t++;

     //m*t - (t*t) - 100*m + 200*t - 10000 == 0
     //solve for t: t == m + 100, t == 100

     }
}

fig1d (Gulwani CAV '09)

#!c
void fig1d(int m){

     int x = 0;
     int y = 0;
     int t = 0;
     while(x < 100 && y < m){
      y++;
      t++;
     }
     while(x < 100 && y >= m){
      x++;
      t++;
     }

     //m*t - (t*t) - 100*m + 200*t - 10000 == 0
     //solve for t: t == m + 100, t == 100
}

fig2a (Gulwani CAV '09)

#!c
/* same as Fig 4_3 Gulwani pldi 09 */

fig2d (Gulwani CAV '09)

#!c
void fig2d(int n, int m){
     //these assertions are based on gulwani pldi fig 4_3
     //(same as cav fig 2a).
     assert (m > 0);
     assert (n > m);

     int x = 0;
     int y = 0;
     int t = 0;
     while(x < n){
      while (y < m){
           t++;
           y++;
      }
      y=0;
      x++;

     }
     //m*n - t == 0, m - n <= -1, -m <= -1
}

fig3a (Gulwani CAV '09)

#!c
void fig3a(int n){
     int x = 0;
     int y = 0;
     int t = 0;
     while(x < n){
      y = x;
      while (y < n){
           t++;
           y++;
      }

      x=y+1;
     }
     //dig2:  n*t - (t*t) == 0, -t <= 0, n - t <= 0
}

fig5b (Gulwani CAV '09)

#!c
void fig5b(int y0, int n){
     int x = 0;
     int y = y0;
     int t = 0;
     while(x < n){
      y++;
      x = x + y;
      t++;

     }
     //(y*y) - (y0*y0) - 2*x + y - y0 == 0, -x <= 0, n - x <= 0, t - y + y0 == 0, -y + y0 <= 0
}

fig1 (Gulwani PLDI '09)

#!c
/*See code in pldi Fig4_1*/

fig2 (Gulwani PLDI '09)

#!c
void fig2(int n, int m, int N){
     assert (0 <= n);
     assert (0 <= m);
     assert (0 <= N);
     int t = 0;
     int i = 0;
     int j = 0;
     int k = 0;
     while(i < n){
      j = 0;
      while(j<m){          
           j = j+1;
           k=i;
           t = t +1;
           while (k<N){         
            k=k+1;
            t = t +1;
           }
           i=k;
      }
      i=i+1;
      t = t + 1;
     }
     //(N*N)*m*n + N*(m*m)*n - N*m*(n*n) - (m*m)*(n*n) - N*m*n*t + m*(n*n)*t + N*m*n - N*(n*n) - 2*m*(n*n) + N*n*t + m*n*t + (n*n)*t - n*(t*t) - (n*n) + n*t == 0, (N*N)*m*t + N*(m*m)*t - N*m*n*t - (m*m)*n*t - N*m*(t*t) + m*n*(t*t) + N*m*t - N*n*t - 2*m*n*t + N*(t*t) + m*(t*t) + n*(t*t) - (t*t*t) - n*t + (t*t) == 0
     //-N <= 0, -m <= 0, -n <= 0, n - t <= 0,        
}

fig2 (Gulwani CAV '09)

#!c
void fig2(int n, int m, int N){
     assert (0 <= n);
     assert (0 <= m);
     assert (0 <= N);
     int t = 0;
     int i = 0;
     int j = 0;
     int k = 0;
     while(i < n){
      j = 0;
      while(j<m){          
           j = j+1;
           k=i;
           t = t +1;
           while (k<N){         
            k=k+1;
            t = t +1;
           }
           i=k;
      }
      i=i+1;
      t = t + 1;
     }
     //%%%traces: int n, int m, int N, int t
     //(N*N)*m*n + N*(m*m)*n - N*m*(n*n) - (m*m)*(n*n) - N*m*n*t + m*(n*n)*t + N*m*n - N*(n*n) - 2*m*(n*n) + N*n*t + m*n*t + (n*n)*t - n*(t*t) - (n*n) + n*t == 0, (N*N)*m*t + N*(m*m)*t - N*m*n*t - (m*m)*n*t - N*m*(t*t) + m*n*(t*t) + N*m*t - N*n*t - 2*m*n*t + N*(t*t) + m*(t*t) + n*(t*t) - (t*t*t) - n*t + (t*t) == 0
     //-N <= 0, -m <= 0, -n <= 0, n - t <= 0
}

fig4_1 (Gulwani PLDI '09)

#!c
void fig4_1(int id, int n){
     assert (id >= 0);
     assert (n > id);
     int tmp = id + 1;
     int t = 0;

     while(tmp != id){
      if (tmp <= n) {
           tmp = tmp + 1;
      }else{
           tmp=0;
      }
      t++;
     }
     //n - t + 1 == 0, -id <= 0, id - n <= -1 
}

fig4_2 (Gulwani PLDI '09)

#!c
void fig4_2(int n, int m){
     assert (n > 0);
     assert (m > 0);
     int v1 = n;
     int v2 = 0;
     int t = 0;
     while(v1 > 0){
      if (v2 < m) {
           v2++;
           v1--;
      }else{
           v2=0;
      }
      t++;
     }

     //m*n - m*t + n - v2 == 0
     //v1 - v2 <= -1, -t + v2 <= 0, -m + v2 <= 0, v1 == 0, 
     //Note: DIG2 cannot find relationship among t and m,n  (annotated n+n/m)
}

fig4_3 (Gulwani PLDI '09)

#!c
//same as fig2a gulwani_cav09

void fig4_3(int n, int m){
     assert (m > 0);
     assert (n > m);
     int i = 0;
     int j = 0;
     int t = 0;
     while(i<n){
      if (j < m) {
           j++;
      }else{
           j=0;
           i++;
      }
      t++;
     }
     //m*n + n - t == 0,
     //-m <= -1, m - n <= -1
}

fig4_4 (Gulwani PLDI '09)

#!c
//todo

fig4_5 (Gulwani PLDI '09)

#!c
void fig4_5(int n, int m, int j){
     assert (m > 0);
     assert (n > m);
     int i = m;
     int t = 0;
     while(i>0 && i < n){
      if (j > 0) {
           i++;
      }else{
           i--;
      }
      t++;
     }
     //%%%traces: int n, int m, int j, int t

     //NOTE: With DIG1 I got m^2*t - m*n*t + n*t^2 - t^3 == 0, whose solutions are t = n-m, t = m, t =0. They seem correct.
     //j plays the role of a fixed truth value representing dir=fwd

     //dig2: (m*m) - m*n + n*t - (t*t) == 0, m - n <= -1, -m <= -1
     //solving for t  [t == -m + n, t == m]

fig2_1 (Gulwani POPL '09)

#!c
void fig2_1(int x0, int y0, int n, int m){

     int x = x0;
     int y = y0;
     int t = 0;
     while(x < n){
      if(y < m){
           y++;
      }
      else{
           x++;
      }
      t++;
     }
}

fig2_2 (Gulwani POPL '09)

#!c

void fig2_2(int x0, int z0, int n){
     int x = x0;
     int z = z0;
     int t = 0;
     while(x < n){
      if(z > x){
           x++;
      }
      else{
           z++;
      }
      t++;
     }
}

fig3_4 (Gulwani POPL '09)

#!c
main fig3_4(int n, int m){
     int x = 0;
     int y = 0;
     int t = 0;
     while((x < n || y < m)){
      if(x < n){
           x++;
           y++;
      }
      else if(y < m){
           x++;
           y++;
      }
      else{
           assert(0);
           break;
      }
      t++;
     }
}

fig4_1 (Gulwani POPL '09)

#!c
void fig4_1(int n, int m){
     assert(m>=0); 
     int x = 0;
     int y = 0;
     int t = 0;
     while(x < n){
      if(y < m){
           y = y + 1;
      }
      else{
           x = x + 1;
      }
      t++;
     }
}

fig4_2 (Gulwani POPL '09)

#!c
void fig4_2(int x0, int y0, int n, int m){
     int x = x0;
     int y = y0;

     int t = 0;
     while(x < n){
      while(y < m){
           y = y + 1;
           t++;
      }
      x = x + 1;
      t++;
     }
}

fig4_3 (Gulwani POPL '09)

#!c
void fig4_3(int n, int m){
    assert(m >= 0);
    assert(n >= 0);
     int x = 0;
     int y = 0;
     int t = 0;
     while(x < n){
      if(y < m){
           y++;
      }
      else{
           y=0;
           x++;
      }
      t++;
     }
}

fig4_4 (Gulwani CAV '09)

#!c
void fig4_4(int n, int m){

     assert(m >= 0);
     assert(n >= 0);
     int x = 0;
     int y = 0;
     int t = 0;
     while(x < n){
      y=0;
      x++;
      while(y < m){
           y++;
           t++;
      }
          t++;
     }
}