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

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

#ifdef _CIVL
$input int ni,nj;
$assume(ni > 1);
$assume(nj > 1);
$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 <= ni;
    @ loop invariant \forall int t; 0 <= t < i ==>
    @                  (\forall int k; 0 <= k < nj ==> u1[t][k]==0 && u2[t][k]==0);
    @ loop invariant i > 0 ==> j == nj;
    @ 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 <= j <= nj;
      @ loop invariant \forall int k; 0 <= 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;
    }
  }

  // straightforward loop nest
  /*@ loop invariant 1 <= i <= ni-1;
    @ loop invariant i == 1 ==> j == nj;
    @ loop invariant i > 1 ==> j == nj - 1;
    @ loop invariant \forall int t; 1 <= t < i ==>
    @                  (\forall int k; 1 <= k < nj-1 ==> u1[t][k] == uin[t][k] * uin[t][k]);
    @ loop assigns   u1[1 .. ni-2][1 .. nj-2], u2[1 .. ni-2][1 .. nj-2], i, j;
    @*/
  for(i=1;i<ni-1;i++) {
    /*@ loop invariant 1 <= j <= nj-1;
      @ loop invariant \forall int k; 1 <= k < j ==> u1[i][k] == uin[i][k] * uin[i][k];
      @ loop assigns u1[i][1 .. nj-2], u2[i][1 .. nj-2], j;
      @*/
    for(j=1;j<nj-1;j++) {
      u1[i][j] = uin[i][j]*uin[i][j];
    }
  }

  if (ni > 2) {
    $assert(i == ni - 1);       
    if (nj > 2)
      $assert(j == nj - 1);
    else
      $assert(j == 1);
  } else {
    $assert(i == 1);
    $assert(j == nj);
  }

  int old_j = j;

  /*@ loop invariant 1 <= i <= ni-1;  
    @ loop invariant 1 < i ==> (nj - 2 <= j <= nj - 1 && j % 2 != 0); // continuous condition I
    @ loop invariant i == 1 ==> j == old_j;                           // continuous condition II
    @ loop invariant \forall int t, k; 1 <= t < i && 1 <= 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 < ni-2;  
    @ loop invariant 1 <= j <= nj-1;
    @ loop invariant \forall int k; 1 <= 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];
    }
  }  

  //$assume(i == 1 => j == old_j);

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