Bill split

A bill in cents is split between people. Everyone pays the same share, rounded up so nobody underpays, and the last person pays what is left. For 1,000 cents between 3 people it gives 334, 334 and 332. But with small shares and many people, rounding up takes more than the whole bill before the last person is reached, and the last share is negative.

src/splitBill.ts

// Splits a bill in cents between people: everyone pays the same share, and the last person pays what is left.
export interface Split {
  each: number;
  last: number;
}

//@ verify
export function splitBill(total: number, people: number): Split {
  //@ requires total >= 0
  //@ requires people >= 1
  //@ ensures \result.each * (people - 1) + \result.last === total
  //@ ensures \result.last >= 0
  //@ ensures \result.each >= 0
  const each = Math.ceil(total / people);
  const last = total - each * (people - 1);
  return { each, last };
}

See how LemmaScript finds and fixes it.