Martin Fowler has a Money class that has a money allocation routine. This routine allocates money according to a given list of ratios without losing any value through rounding. It spreads any remainder value over the results.
For example, $100 allocated by the "ratios" (1, 1, 1) would yield ($34, $33, $33).
Here is the allocate
function:
public long[] allocate(long amount, long[] ratios) {
long total = 0;
for (int i = 0; i < ratios.length; i++) total += ratios[i];
long remainder = amount;
long[] results = new long[ratios.length];
for (int i = 0; i < results.length; i++) {
results[i] = amount * ratios[i] / total;
remainder -= results[i];
}
for (int i = 0; i < remainder; i++) {
results[i]++;
}
return results;
}
(For the sake of this question, to make it simpler, I've taken the liberty of replacing the Money types with longs.)
The question is, how do I know it is correct? It all seems pretty self-evident except for the final for-loop. I think that to prove the function is correct, it would be sufficient to prove that the following relation is true in the final for-loop:
remainder < results.length
Can anyone prove that?