Belegten Stand und lebenslange Zahl erfolgreicher Verbräuche unterscheiden.
Eine Rückgabe senkt used, im betrachteten Vertrag jedoch nie unter null. Damit beschreibt das Budget belegte beziehungsweise noch nicht zurückgegebene Einheiten. Es ist keine unveränderliche Obergrenze für alle jemals erfolgreichen consume-Aufrufe: Nach einer Rückgabe kann ein neuer Verbrauch gelingen. Lege deshalb fest, wann eine Einheit tatsächlich zurückgegeben werden darf. Wird für dieselbe Arbeit doppelt erstattet, kann der Zähler zwar nicht negativ werden und dennoch freien Platz vortäuschen. Die Zahleninvariante ist notwendig; die Zuordnung einer Rückgabe zu einer zuvor belasteten Arbeit ist ein zusätzlicher fachlicher Vertrag.
Ein Beispiel
Grenze 2: Paket A verbraucht einen Platz, Paket B den zweiten. A wird vor Beginn verworfen und gibt seinen Platz einmal zurück; Paket C kann ihn nutzen. Es gab nun drei erfolgreiche Verbräuche, used bleibt 2. Eine weitere Rückgabe für A wäre fachlich falsch, selbst wenn die Untergrenze den Zähler bei null schützen würde.
