Prove initiation and preservation with a strong enough invariant

Let Init identify permitted starting states and Next relate current and successor states. An inductive predicate J must hold initially and remain true after every Next step from a J-state. If J implies the desired safety predicate P, the induction establishes P for all reachable states. Preservation examines every state satisfying J, including states that might not be reachable from Init. This wider domain is why a preservation counterexample can reveal an insufficient hypothesis rather than a genuine executable failure from the initial state.

Include type and domain facts in J rather than relying on a variable's informal name. A free-capacity field intended to be an integer needs that constraint in the reasoning. Check all action cases, including duplicate requests, cancellation, recovery, and stuttering. Initialization must cover every allowed initial state, not just one convenient example. An invariant that holds only after a startup transition needs either a different initial model or an additional argument establishing the transition and the invariant before the contract begins.

For the reservation service, the desired bound is that held plus committed units never exceed capacity. That predicate alone allows an artificial state with capacity two, two occupied units, and one free unit. The Reserve guard sees the free unit and permits a third occupied unit. This state cannot arise under the correct conservation rule, but the weak induction hypothesis has not excluded it. Add conservation, nonnegative free capacity, status partitioning, and stable request domains to the strengthening, then revisit initiation and every action case.

For Reserve, occupied count increases by one while free capacity decreases by one; the positive-free guard keeps the new free count nonnegative. Commit preserves total occupied count while changing its status class. Cancel transfers a held unit back to free capacity. A duplicated cancellation must have no refund transition from a terminal status. These local calculations preserve the strengthened relationship, from which the desired bound follows. This is a mechanism-level explanation; merely declaring the bound as an invariant to check does not supply the induction argument.

A checker started from Init can expose a reachable invariant violation within its configured search. A checker started from J to test preservation can instead expose a state admitted by J but unreachable from Init. Inspect the starting predicate and trace before deciding whether to repair the protocol or strengthen the candidate invariant. An overstrong invariant can fail initiation by excluding legitimate starts; an understrong one can fail preservation or fail to imply P. Every changed strengthening needs all three obligations checked again under the same domains and assumptions.

The function instrument offers a small domain reminder. Reset, set coefficient a=1 and position x=1, predict y=1, then Play or Step. Separately Reset, set a=1 and x=−1, predict the same y=1 but tangent slope −2 rather than +2, then Play or Step. One output value does not capture all state facts relevant to the next claim. This fixed quadratic is not an invariant prover and has no reservation actions. It only illustrates why a summary can omit distinctions required by a preservation argument.