int t[8];


/*@
   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 invariant \forall integer j ; (0 <= j < i) ==> (t[j] == 2) ;
       loop variant 8 - i ;
  */
   for(i = 0; i <8; i++)
     {
       t[i] += 1;
     }
}