{n:nat}
unit intcopy(size: int(n), int src[n], int dst[n]) {
  var: int ind;;
  invariant: [i:int | 0 <= i <= n] (ind: int(i))
/*
  while (ind < size) {
    dst[ind] = src[ind]; ind = ind + 1;
  }
*/
  for (ind = 0; ind < size; ind = ind + 1) {
    dst[ind] = src[ind];
  }
}