void arrayinit(int A[], unsigned len)
_(writes \array_range(A,len))
_(ensures \forall unsigned k; k < len ==> A[k] == 0)
{
  unsigned i = 0;
  while (i < len)
  _(invariant \forall unsigned l; l < i ==> A[l] == 0)
  {
    A[i] = 0;
    i++;
  }
}