/*@ requires a >= 0 && b > 0;
  assigns \nothing;
  ensures 0 <= \result < b &&
  \exists int q; a == b * q + \result;
 */
int remainder (int a, int b) {
  int r = a;
  /*@ loop invariant r >= 0 && \exists integer q; a == b * q + r;
    loop assigns r; */
  while (r >= b)
    r = r - b;
  return r;
}