#define CAPACITY 1000000
/*@ logic integer size_rec(int* busybits, integer capa) = 
  @   (capa <= 0) ? 0 :
  @   (busybits[capa-1] != 0) ? 1 + size_rec(busybits, capa - 1) :
  @   size_rec(busybits, capa - 1);
*/

/*@ requires \valid(busybits + {i | integer i; 0 <= i < CAPACITY});
  @ assigns \nothing;
  @ ensures \result == size_rec(busybits, CAPACITY);
  @ ensures 0 <= \result < CAPACITY;
*/
int size(int busybits[CAPACITY]) {
    int s = 0;
    /*@ loop invariant \valid(busybits + {i | integer i; 0 <= i < CAPACITY});
      @ loop invariant s == size_rec(busybits, i);
      @ loop assigns i;
      @ loop variant (CAPACITY - i);
    */
    for (int i = 0; i < CAPACITY; ++i) {
        int bb = busybits[i];
        if (1 == bb) {
            ++s;
        }
    }
    return s;
}