证明Fowler的资金分配算法是正确的

马丁福勒 has a Money class 这有一个资金分配程序。此例程根据给定的比率列表分配资金,而不会因四舍五入而损失任何值。它将任何余数值分散到结果上。

例如,“比率”(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替换了货币类型。)

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

remainder < results.length

有人能证明吗?