证明福勒的资金分配算法是正确的
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;
}
为了解决这个问题，为了让它更简单，我冒昧地将 Money 类型替换为 long。）
问题是，我怎么知道它是正确的吗？除了最后的 for 循环之外，这一切似乎都是不言而喻的。我认为要证明该函数是正确的，只需在最后的 for 循环中证明以下关系成立就足够了：
remainder < results.length
有人能证明这一点吗？
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?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（4）
关键的见解是，计算每个结果[i]时，总余数等于各个余数的总和。
由于每个余数都是向下取整的结果，因此最多为 1。这样的余数有
results.length个，因此总余数最多为results.length。编辑：显然，如果没有一些漂亮的符号，这不是一个证明，所以这里有一些......
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.lengthsuch remainders, so the total remainder is at mostresults.length.EDIT: Obviously it's not a proof without some pretty symbols, so here are some...
无需证明。
基本金额通过简单除法分配，向下舍入。
因此分配的金额将始终小于或等于总数。
剩余部分包含未分配的金额。这始终是小于“i”的整数。所以他只是给每个接收者 1，直到钱用完为止。
No proof required.
The base amounts are allocated by simple division, rounding down.
So the allocated amount will always be less than or equal to the total.
Remainder contains the unallocated amount. Which will always be a whole number less than 'i'. So he simply gives each receiver 1 until the money is gone.
简单
，只需使用
a=floor(a/b)*b+(a%b)
Simple
just use fact that
a=floor(a/b)*b+(a%b)
我想说这是不正确的，因为某些奇怪的比率可能会导致余数大于结果数。因此我建议results[i % results.length].amount++;.编辑：我撤回我的答案。对于多头，没有奇怪的比率，对于浮点模没有帮助
I'd say it's not correct because some curious ratio could cause a remainder greater then the number of results. Therefore I suggestresults[i % results.length].amount++;.Edit: I withdraw my answer. With longs there's no curious ratio and with floating point modulo doesn't help