Beweisen Sie, dass Fowlers Geldallokationsalgorithmus korrekt ist

Question

Martin Fowler has a Money class, der eine Geldzuweisungsroutine hat. Diese Routine teilt Geld gemäß einer gegebenen Liste von Verhältnissen zu, ohne irgendeinen Wert durch Runden zu verlieren. Es verteilt jeden Restwert über die Ergebnisse.

Zum Beispiel würde $ 100 durch die "Ratios" (1, 1, 1) zugewiesen ergeben ($ 34, $ 33, $ 33). Hier

ist die allocate Funktion:

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

(. Für die Zwecke dieser Frage, es einfacher zu machen, habe ich mir die Freiheit für den Ersatz der Geldtypen mit longs genommen)

Die Frage ist, woher weiß ich, dass es richtig ist? Alles scheint ziemlich selbstverständlich zu sein, außer für die finale For-Schleife. Ich denke, dass die Funktion zu beweisen, richtig ist, wäre es ausreichend, um zu beweisen, daß die folgende Beziehung in dem endgültigen for-Schleife erfüllt ist:

remainder < results.length 

Kann das jemand beweisen?

Answer 1

Die wichtigste Erkenntnis ist, dass der Gesamtrest gleich der Summe der einzelnen Reste bei der Berechnung jeder result[i] ist.

Da jeder einzelne Rest das Ergebnis der Abrundung ist, ist es höchstens 1. Es gibt results.length solche Reste, so dass der Gesamtrest höchstens results.length ist.

EDIT: Offensichtlich ist es nicht ein Beweis, ohne ein paar ziemlich Symbole, so dass hier einige sind ...

Answer 2

Ich würde sagen, es ist nicht korrekt, weil ein seltsames Verhältnis einen Rest verursachen könnte, der größer ist als die Anzahl der Ergebnisse. Daher schlage ich results[i % results.length].amount++; vor.

Edit: Ich ziehe meine Antwort zurück. Mit longs gibt es kein merkwürdiges Verhältnis und mit Fließkomma hilft modulo nicht

Answer 3

Kein Beweis erforderlich.

Die Basisbeträge werden durch einfache Division, Abrunden zugeordnet. Der zugewiesene Betrag wird also immer kleiner oder gleich dem Gesamtbetrag sein.

Rest enthält die nicht zugewiesene Menge. Das wird immer eine ganze Zahl weniger als 'ich' sein. Also gibt er jedem Empfänger einfach 1, bis das Geld weg ist.

Answer 4

Einfache

gerade Tatsache nutzen, dass

a = Boden (a/b) * b + (a% b)