int t[8];

/* Q0: Write the assigns clause in the contracts of functions init, incr, main.
   Q1: Verify the safety of function init.
   Q2: Verify the ACSL contract of function init. */

/*@ 
  assigns t[0..7] ;
  ensures \forall integer i ; (0 <= i <= 7) ==> (t[i] == 1) ;
*/
void init(void)
{
  int i;
  /*@ loop invariant \forall integer j ; (0 <= j < i) ==> (t[j] == 1) ;
      loop invariant 0 <= i <= 8 ; 
      loop variant 8 - i ; */
  for(i = 0; i < 8; i++)
    t[i] = 1;
}






/* Q3: Verify the safety of function incr.
   Q4: Verify the ACSL contract of function incr. */

/*@ 
  requires \forall integer i ; (0 <= i <= 7) ==> (t[i] == 1) ;
  assigns t[0..7] ;
  ensures \forall integer i ; (0 <= i <= 7) ==> (t[i] == 2) ;
*/
void incr(void)
{
  int i;
  /*@
      loop invariant -1 <= i <= 7 ; 
      loop variant i + 1; 
      loop invariant \forall integer j ; (i < j <= 7) ==> (t[j] == 2) ;
      loop invariant \forall integer j ; (0 <= j <= i) ==> (t[j] == 1) ;
 */
  for(i = 7; i >= 0; i--)
    {
      t[i] += 1;
    }
}

/*@ 
  requires \forall integer i ; (0 <= i <= 7) ==> (t[i] == 1) ;
  assigns t[0..7] ;
  ensures \forall integer i ; (0 <= i <= 7) ==> (t[i] == 2) ;
*/
void incr2(void)
{
  int i;
  /*@
      loop invariant 0 <= i <= 8 ; 
      loop assigns i, t[0..i-1] ;
      loop variant 8 - i ; 
      loop invariant \forall integer j ; (0 < j < i) ==> (t[j] == 2) ;
 */
  for(i = 0; i <8; i++)
    {
      t[i] += 1;
    }
}

/* Q5: Verify the ACSL contract of function main. */

/*@ 
  assigns t[0..7] ;
  ensures \forall integer i ; (0 <= i <= 7) ==> (t[i] == 2) ;
*/
void main(void)
{
  init();
  incr();
}