18Verification

Bound a method with readiness

Problem

bump is the resource boundary for a counter that may advance only while its value is below three. The starter defines the method with no readiness condition, so the calling drive rule remains enabled for all five attempts and the public run reaches five.

Add the missing condition to the bump method header. Do not move the bound into drive, change the counter width or initial value, or add control state. The method itself must protect every caller.

Navigate the starter

Read BoundedCounter first: it promises one action method and one observable value method. In mkBoundedCounter, locate the state changed by bump. Then read mkTop in this order: drive makes the call, advance counts five observation cycles independently, and show reports the final counter.

Before editing, predict both rule enables. With unconditional readiness, drive and advance can run while cycles < 5; the counter advances on every attempt. After the correction, advance can still reach five, but the implicit condition from bump must disable the complete drive action once the counter reaches its bound.

Make and explain the minimal change

A method guard contributes to the composite condition of every rule that calls the method. Put the state-dependent bound at that shared boundary. The method body already performs the correct one-step update, and the caller already has the correct attempt window.

Use Run, then account for all five cycles:

Entry counter	Method ready?	Effect of the calling rule
0	yes	One call commits counter 1.
1	yes	One call commits counter 2.
2	yes	One call commits counter 3.
3	no	The whole caller is disabled; the counter stays 3.
3	no	The caller remains disabled while `advance` finishes.

Completion is not merely seeing three once. The counter must begin at zero, make exactly three successful one-step transitions, remain at three on later attempt cycles, and apply the same protection to any rule that calls bump. A caller-local if can match the visible sample while violating that reusable method contract.

Progressive hints

Hint 1 — identify the contract owner

Ask which declaration should decide whether any caller may mutate count. The restriction belongs with the operation that owns that mutation.

Hint 2 — locate the syntax

The editable point is the existing bump method header, between its empty argument list and the terminating semicolon. Its body needs no change.

Hint 3 — choose the predicate

Use a comparison between the current counter and the exclusive upper bound. The condition must still be true at two and become false at three.

Transfer experiment

After the required version works, change only the method's bound from three to four and predict the final public value before running. advance should still complete five observation cycles, while drive gains exactly one successful call. This ungraded variation checks that readiness, rather than copied caller control, determines progress.