09Implementation

Define a private package constant

Read and predict

Meter publishes charge, total, remaining and full. Everything those methods agree on comes from budget, a package-level constant that sits outside every module and that no caller can see.

budget is still a don't-care value at the TODO. The public driver charges three units at a time, so its fixed-size requests must stop once twelve units are spent, with remaining at zero and full true.

Trace the same budget name through the readiness condition, remaining, and full. Before editing, predict why a don't-care package constant prevents those three observations from describing one reliable policy.

Repair path

Set the package-level definition only. Keep the method bodies and reports tied to that name. Run and follow the state sequence from zero through four accepted charges; at the boundary, total, remaining, and full must agree.

Completion contract

Define budget as twelve.
Keep budget at package level so the guard and both reports read one value.
Do not repeat the bound as a literal inside the module.
Preserve the accepted-call boundary as well as the final reports; extra charges hidden by a hard-coded display are not valid.

Progressive hints

Hint 1

A package-level constant is a plain typed definition outside any module, so first identify every consumer of budget.

Hint 2

charge accepts three units at a time and must stop at twelve, so four calls succeed.

Concept

A package-level constant belongs to the package, not to any module in it. One definition can steer a method's readiness and everything the interface reports, while remaining invisible to callers.

Transfer experiment

After completing the task, reason about changing the charge amount from three to five while keeping a budget of twelve. The current readiness condition can accept a request that crosses the budget because it tests only the prior state. Do not change the graded solution; use this variation to distinguish a fixed-size protocol from a general request-fit policy.