{size:nat}
unit init (vec: <int> array(size)) {
  var: int i, n;;

  i = 0; n = vec.size;

  invariant: [i:nat, n:nat | i + n = size] (i: int(i), n: int(n))
  while (0 < n) {
    vec.data[i] = 0;
    i =  i + 1; n = n - 1;
  }
}