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

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

#ifdef _CIVL
$input int ni,nj;
$assume(ni>0);
//$assume(ni<10);
$assume(nj>0);
//$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];
  
  /*@ loop invariant 0 <= i && i <= ni; 
    @ loop invariant \forall int t; 0 <= t && t < i ==> 
    @                               (\forall int k; 0 <= k && k < nj ==>
    @                                  u1[t][k] == 0 && u2[t][k] == 0);
    @ loop assigns   u1[0 .. ni-1][0 .. nj-1], u2[0 .. ni-1][0 .. nj-1], i, j;
    @*/
  for(i=0;i<ni;i++) {
  /*@ loop invariant 0 <= i && i < ni; 
    @ loop invariant 0 <= j && j <= nj; 
    @ loop invariant \forall int k; 0 <= k && k < j ==>
    @                                  u1[i][k] == 0 && u2[i][k] == 0;
    @ loop assigns   u1[i][0 .. nj-1], u2[i][0 .. nj-1], j;
    @*/
    for(j=0;j<nj;j++) {
      u1[i][j] = 0;
      u2[i][j] = 0;
    }
  }
  $assert($forall (int i : 0 .. ni-1) 
          ($forall (int j : 0 .. nj-1) u1[i][j] == 0 && u2[i][j] == 0)
          );
}