Доказательство правильности алгоритма распределения денег Фаулера

Мартин Фаулер имеет класс Money, который имеет рутину распределения денег. Эта процедура распределяет деньги в соответствии с определенным списком коэффициентов, не теряя при этом значения при округлении. Он распределяет любое остаточное значение по результатам.

Например, 100 долларов, выделенных "отношениями" (1, 1, 1), будут давать ($ 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;
}

(Ради этого вопроса, чтобы сделать его проще, я взял на себя смелость заменить типы денег длинными.)

Вопрос в том, как я знаю, что это правильно? Все это кажется довольно очевидным, за исключением финальной петли. Я думаю, что для доказательства правильности функции было бы достаточно доказать, что в заключительном for-loop истинно следующее соотношение:

remainder < results.length

Кто-нибудь может это доказать?

Ответы

Ответ 1

Ключевое понимание состоит в том, что общий остаток равен сумме отдельных остатков при расчете каждого result[i].

Так как каждый отдельный остаток является результатом округления, он не более 1. Есть такие t12, что общий остаток не превышает results.length.

РЕДАКТИРОВАТЬ: Очевидно, это не доказательство без каких-либо симпатичных символов, поэтому вот некоторые из них...

Ответ 2

Не требуется никаких доказательств.

Базовые суммы распределяются простым делением, округлением вниз. Таким образом, выделенная сумма всегда будет меньше или равна сумме.

Остальное содержит нераспределенную сумму. Который всегда будет целым числом меньше, чем "i". Поэтому он просто дает каждому получателю 1, пока деньги не исчезнут.

Ответ 3

Я бы сказал, что это не правильно, потому что какое-то любопытное отношение может привести к тому, что остаток будет больше, чем количество результатов. Поэтому я предлагаю results[i % results.length].amount++;.

Изменить: я снимаю свой ответ. С longs нет никакого любопытного отношения и с модулем с плавающей запятой не помогает

Ответ 4

Простой

просто используйте факт, что

а = пол (A/B) * B + (а% б)