source: CIVL/examples/loop_invariants/Jans_example/fixed_block/invariant_3rd_loop.cvl

#include <stdio.h>
#ifdef _CIVL
#include <civlc.cvh>
#pragma CIVL ACSL
#endif

#ifdef _CIVL
$input int ni,nj;
$assume(ni>1);
//$assume(ni<10);
$assume(nj>1);
//$assume(nj<10);
$input double uin[ni][nj];
#endif

int main(int argc, char** argv) {
  int i,j,ir,jr;
  double u1[ni][nj];
  double u2[ni][nj];
  
  $assume($forall (int i : 0 .. ni-1) 
          ($forall (int j : 0 .. nj-1) u1[i][j] == 0 && u2[i][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 1 <= i && i <= ni-1;  
    @ loop invariant \forall int t, k; 1 <= t && t < i && 1 <= k && k < nj - 2 && k % 2 != 0
    @                     ==> u2[t][k] == uin[t][k]*uin[t][k] && u2[t][k+1] == uin[t][k+1]*uin[t][k+1];
    @ loop invariant i % 2 != 0;
    @ loop assigns u2[1 .. ni-2][1 .. nj-2], i, j;
    @*/
  for(i=1;i<ni-2;i=i+2) {
  /*@ loop invariant 1 <= i && i < ni-2;  
    @ loop invariant 1 <= j && j <= nj-1;
    @ loop invariant \forall int k; 1 <= k && k < j 
    @                  ==> u2[i][k] == uin[i][k]*uin[i][k] && u2[i+1][k] == uin[i+1][k]*uin[i+1][k] ;
    @ loop invariant i % 2 != 0 && j % 2 != 0;
    @ loop assigns u2[i][1 .. nj-2], u2[i+1][1 .. nj-2], j;
    @*/
    for(j=1;j<nj-2;j=j+2) {
      u2[i][j] = uin[i][j]*uin[i][j];
      u2[i+1][j] = uin[i+1][j]*uin[i+1][j];
      u2[i][j+1] = uin[i][j+1]*uin[i][j+1];
      u2[i+1][j+1] = uin[i+1][j+1]*uin[i+1][j+1];
    }
  }  
  $assert($forall (int i | 1 <= i && i < ni - 2 && i % 2 != 0) 
          ($forall (int j | 1 <= j && j < nj - 2 && j % 2 != 0)
           u2[i][j] == uin[i][j]*uin[i][j] &&
           u2[i+1][j] == uin[i+1][j]*uin[i+1][j] &&
           u2[i][j+1] == uin[i][j+1]*uin[i][j+1] &&
           u2[i+1][j+1] == uin[i+1][j+1]*uin[i+1][j+1])
          );
}