#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; }