Search code examples
algorithmcurrencyallocationproof

Proof that Fowler's money allocation algorithm is correct

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?

Solution

  • The key insight is that the total remainder is equal to the sum of the individual remainders when calculating each result[i].

    Since each individual remainder is the result of rounding down, it is at most 1. There are results.length such remainders, so the total remainder is at most results.length.

    EDIT: Obviously it's not a proof without some pretty symbols, so here are some...
    alt text