source: CIVL/examples/loop_invariants/Jans_example/arbitrary_block/arbitrary_block-bad_invariants1.cvl

#pragma CIVL ACSL
#include "loop_bounds.cvl"
$input int ni,nj,bi,bj;
$assume(0<bi && bi<ni && 0<bj && bj<nj);
$input double uin[ni][nj];
$input double u1[ni][nj];
double u2[ni][nj];
instantiate_theory_loop_bounds(ni,bi,1);
instantiate_theory_loop_bounds(nj,bj,1);

int main() {
    int i=0,j=1,ir,jr,ib,jb;

    $assume($forall (int i : 0 .. ni-1) u1[i][0] == 0 && u1[i][nj-1] == 0);
    $assume($forall (int j : 0 .. nj-1) u1[0][j] == 0 && u1[ni-1][j] == 0);
    $assume($forall (int i : 1 .. ni-2) ($forall (int j : 1 .. nj-2) u1[i][j] == uin[i][j] * uin[i][j]));

    /*@ loop invariant in_range(i, 1, ni-bi, bi);
      @ loop invariant 1 <= j <= loop_max(1, nj-bj, bj);        // frame condition for j
      @ loop invariant \forall int t; 1 <= t < i  ==>
      @                   (\forall int j0; 1 <= j0 < loop_max(1, nj-bj, bj) ==> 
      @                       u2[t][j0] == uin[t][j0]*uin[t][j0]);
      @ loop assigns i, j, ib, jb, u2[1 .. ni - 2][1 .. nj - 2];
      @*/
    for(i=1;i<ni-bi;i=i+bi) {    
      /*@ loop invariant in_range(j, 1, nj-bj,bj);
        @ loop invariant \forall int t; i <= t < i + bi ==>
        @                   (\forall int j0; 1 <= j0 < j ==> 
        @                       u2[t][j0] != uin[t][j0]*uin[t][j0]);
        @ loop assigns j, ib, jb, u2[i .. i + bi - 1][1 .. nj - 2];
        @*/
      for(j=1;j<nj-bj;j=j+bj) {
        /*@ loop invariant 0 <= ib <= bi;
          @ loop invariant \forall int t; i <= t < i + ib ==> 
          @                   (\forall int k; j <= k < j + bj ==> u2[t][k] == uin[t][k]*uin[t][k]);
          @ loop assigns   ib, jb, u2[i .. (i + bi - 1)][j .. (j + bj - 1)];
          @*/
        for(ib=0;ib<bi;ib++) {
          /*@ loop invariant 0 <= jb <= bj;
            @ loop invariant \forall int k; j <= k < j + jb ==> u2[i+ib][k] == uin[i+ib][k]*uin[i+ib][k];
            @ loop assigns   jb, u2[i + ib][j .. (j + bj - 1)];
            @*/
          for(jb=0;jb<bj;jb++) {
            u2[i+ib][j+jb] = uin[i+ib][j+jb]*uin[i+ib][j+jb];
          }
        }
      }
    }
    $assert(i == loop_max(1,ni-bi,bi));
    $assert($forall (int i0 | 1 <= i0 && i0 < loop_max(1,ni-bi, bi)) 
            $forall (int j0 | 1 <= j0 && j0 < j) u2[i0][j0] == uin[i0][j0]*uin[i0][j0]);

    // remainder i
    /*@ loop invariant i <= ir <= ni-1;
      @ loop invariant \forall int t; i <= t < ir ==>
      @                  (\forall int k; 1 <= k < loop_max(1, nj - bj, bj) ==>
      @                     u2[t][k] == uin[t][k]*uin[t][k]);
      @ loop assigns ir, jr, jb, u2[i .. ni - 2][1 .. nj - 2];
      @*/
    for(ir=i;ir<ni-1;ir++) {
      /*@ loop invariant in_range(jr, 1, nj-bj, bj);
        @ loop invariant \forall int t; 1 <= t < jr ==>
        @                               u2[ir][t] == uin[ir][t]*uin[ir][t];
        @ loop assigns jr, jb, u2[ir][1 .. nj - 2];
        @*/      
      for(jr=1;jr<nj-bj;jr=jr + bj) {
        /*@ loop invariant 0 <= jb <= bj;
          @ loop invariant \forall int t; jr <= t < jr + jb ==>
          @                               u2[ir][t] == uin[ir][t]*uin[ir][t];
          @ loop assigns jb, u2[ir][jr .. jr+bj-1];
          @*/
        for(jb=0;jb<bj;jb++) {
          u2[ir][jr+jb] = uin[ir][jr+jb]*uin[ir][jr+jb];
        }
      }
    }
    
    $assert($forall (int i0 | loop_max(1,ni-bi,bi) <= i0 && i0 < ni - 1) 
            $forall (int j0 | 1 <= j0 && j0 < j) u2[i0][j0] == uin[i0][j0] * uin[i0][j0]);

    // remainder j
    /*@ loop invariant j <= jr <= nj-1;
      @ loop invariant \forall int t; 1 <= t < loop_max(1, ni - bi, bi) ==>
      @                   (\forall int k; j <= k < jr ==>
      @                      u2[t][k] == uin[t][k]*uin[t][k]);
      @ loop assigns jr, ir, ib, u2[1 .. ni - 2][j .. nj-2];
      @*/
    for(jr = j; jr < nj-1; jr++) {
      /*@ loop invariant in_range(ir, 1, ni-bi, bi);
        @ loop invariant \forall int t; 1 <= t < ir ==>
        @                               u2[t][jr] == uin[t][jr]*uin[t][jr];
        @ loop assigns ir, ib, u2[1 .. ni - 2][jr];
        @*/
      for(ir = 1; ir < ni-bi; ir+=bi) {
        /*@ loop invariant 0 <= ib <= bi;
          @ loop invariant \forall int t; ir <= t < ir + ib ==>
          @                               u2[t][jr] == uin[t][jr]*uin[t][jr];
          @ loop assigns ib, u2[ir .. ir + bi - 1][jr];
          @*/
        for(ib = 0; ib < bi; ib++) {
          u2[ir+ib][jr] = uin[ir+ib][jr]*uin[ir+ib][jr];
        }
      }
    }

    $assert($forall (int i0 | 1 <= i0 && i0 < loop_max(1, ni-bi, bi)) 
            $forall (int j0 | j <= j0 && j0 < nj - 1) u2[i0][j0] == uin[i0][j0] * uin[i0][j0]);
    
    // remainder ij

    /*@ loop invariant i <= ir <= ni-1;
      @ loop invariant \forall int t; i <= t < ir ==>
      @                  (\forall int k; j <= k < nj-1 ==> u2[t][k] == uin[t][k]*uin[t][k]);
      @ loop assigns ir, jr, u2[i .. ni-2][j .. nj-2];
      @*/
    for(ir = i;ir < ni-1;ir++) {
      /*@ loop invariant j <= jr <= nj-1;
        @ loop invariant \forall int t; j <= t < jr ==> u2[ir][t] == uin[ir][t]*uin[ir][t];
        @ loop assigns jr, u2[ir][j .. nj-2];
        @*/
      for(jr = j;jr < nj-1;jr++) {
        u2[ir][jr] = uin[ir][jr]*uin[ir][jr];
      }
    }
    
    $assert($forall (int i0 | i <= i0 && i0 < ni-1)
            $forall (int j0 | j <= j0 && j0 < nj-1) u2[i0][j0] == uin[i0][j0]*uin[i0][j0]);

    // final assertion:
    $assert($forall (int i : 0 .. ni-1)  $forall (int j : 0 .. nj-1) u1[i][j] == u2[i][j]);
}