证明福勒的货币分配算法是正确的

Question

Martin Fowler 有一个Money类,有一个货币分配程序.该例程根据给定的比率列表分配资金,而不会通过舍入而损失任何价值.它会将任何余数值传播到结果上.

例如,由"比率"(1,1,1)分配的100美元将产生(34美元,33美元,33美元).

这是allocate功能:

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;
}

(为了这个问题,为了简单起见,我冒昧地用long取代Money类型.)

问题是,我怎么知道它是正确的？除了最终的for-loop之外,这一切似乎都是不言而喻的.我认为,为了证明函数是正确的,在最终的for循环中证明以下关系是正确的就足够了:

remainder < results.length

谁能证明这一点？

Answer 1

关键的见解是总余数等于计算每个余数时各个余数的总和result[i].

由于每个单独的余数是四舍五入的结果,因此最多为1.存在results.length这样的余数,因此总余数最多results.length.

编辑:显然这不是没有一些漂亮符号的证据,所以这里有一些......