Invariants and checking¶
A model can describe an intended payment and still allow an unintended one. Checking asks whether a stated property holds for the behaviors explored under a particular configuration. Understanding that configuration is part of understanding the result.
The state introduction explains the notation used here. The payment example uses a nonnegative balance, an explicit payment event and a completion boundary.
An invariant describes every reachable state¶
An invariant is a predicate on a state. A balance invariant can require:
available >= 0
Read it as “the balance is nonnegative in every state this model can reach.” To investigate it, a checker needs starting states and permitted steps, not just the predicate itself.
An invariant can miss a defect when it asks too little. A faulty action might spend tokens without recording payment and still preserve a nonnegative balance. That requires another property about commitment or history. A collection of green results is useful only to the extent that its properties distinguish the failures that matter.
Prepared assertions and exploration establish different things¶
An assertion can evaluate a formula for a prepared example, such as a cost with one increase and one reduction. It answers that concrete question. A transition model can instead start from an initial state, follow enabled actions and explore reachable states.
Evidence class |
Question it can address |
Required context |
|---|---|---|
Prepared assertion |
Does this expression have the expected value for the supplied inputs? |
The exact examples and assertions. |
Finite state exploration |
Does this property hold in the reachable states of this finite model? |
Initial states, actions, bounds, constraints and properties. |
Temporal check |
Do the explored behaviors satisfy a property over time? |
The behavior model, fairness assumptions and finite configuration. |
A model-checking result is not a deductive proof over every possible input size. This reference uses each result’s stated class and scope rather than treating all checking as one kind of proof.
A safety claim does not guarantee progress¶
“No balance becomes negative” is a safety claim: a bad event never occurs. “A pending payment eventually completes” is a progress claim: something must happen later.
A model that permits a pending state to repeat forever may preserve every balance invariant while failing the progress claim. A temporal result must explain whether the environment is assumed to offer completion and whether an enabled completion must eventually be chosen. Fairness assumptions express such scheduling requirements; they are additional parts of the claim.
Stuttering means a step leaves the modeled variables unchanged. It can account for activity outside the chosen abstraction. Allowing stuttering is not the same as guaranteeing that useful work eventually resumes.
Read a counterexample as evidence about a named property¶
A safety counterexample is a sequence reaching a state that violates the checked property. Read it from the starting state, identify the decisive step, and compare that step with the intended contract. A temporal counterexample may also include a repeating loop or a stuttering suffix; omitting that part changes its meaning.
A deliberately defective companion can test whether a property catches a specific mistake. Its failure is useful only when the expected property and diagnostic actually occur. A parser error, exhausted resource limit or interrupted run is not a successful negative control.
An authored example is not a counterexample trace. A passing result does not necessarily emit a witness trace. Evidence without an admitted trace should retain its model and result links without inventing an execution to display.
Check the receipt before transferring the claim¶
Follow a result to its exact source, configuration, tool identity, command, bounds, properties, outcome and assumptions. Check whether exploration completed and whether constraints excluded relevant states. A finite supply of test identities is a model bound; it does not automatically make the intended game resource finite.
The payment evidence page is the destination for results about the payment package. Its recorded outcome, when available, governs the checking claim. This chapter itself records no execution or passing result.
Now read resources and payment and separate three questions: what the cost is, whether payment is allowed, and what becomes true when payment commits.