A prova de que algoritmo de alocação de dinheiro de Fowler está correto

Question

Martin Fowler tem uma classe Dinheiro que tem uma rotina de alocação de dinheiro. Este dinheiro aloca de rotina de acordo com uma determinada lista de razões sem perder qualquer valor através de arredondamento. Ele se espalha qualquer valor restante sobre os resultados.

Por exemplo, US $ 100 atribuída pelos "índices" (1, 1, 1) renderia ($ 34, $ 33, $ 33).

Aqui é a função 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;
}

(Por causa desta questão, para torná-lo mais simples, eu tomei a liberdade de substituir os tipos de dinheiro com longs.)

A questão é, como é que eu sei que é correto? Tudo parece bastante auto-evidente exceto para o loop for final. Eu acho que para provar a função está correta, seria suficiente para provar que a seguinte relação é verdade no final para-loop:

remainder < results.length

Alguém pode provar isso?

Answer 1

O aspecto chave é que o restante total é igual à soma dos restos individuais no cálculo de cada result[i].

Uma vez que cada indivíduo restante é resultado de arredondamento para baixo, é, no máximo, 1. Há results.length esses restos, então o restante total é de, no máximo, results.length.

EDIT: Obviamente não é uma prova sem alguns símbolos bonitas, por isso aqui estão alguns ...

Answer 2

Nenhuma prova necessária.

Os valores de base são alocados por divisão simples, arredondando para baixo. Assim, o montante atribuído será sempre menor ou igual ao total.

Restante contém a quantidade não alocado. Que será sempre um número inteiro inferior a 'i'. Então ele simplesmente dá a cada receptor 1 até que o dinheiro está desaparecido.

Answer 3

Simples

uso apenas fato de que

= um andar (a / b) * + b (em% b)

Answer 4

Eu diria que não é correto porque alguns relação curiosa poderia causar uma maior restante, em seguida, o número de resultados. Portanto, sugiro results[i % results.length].amount++;.

Edit: eu retirar minha resposta. Com longs não há nenhuma razão curiosa e com módulo de ponto flutuante não ajuda