Learn¶
Build a mechanism from its state, the changes it permits and the claims made about it. These chapters introduce notation at its first use. No knowledge of another game’s rules or vocabulary is needed.
Foundations and small teaching models¶
Reading a model: find a before/after change, its guard and unchanged fields.
Values and state: distinguish numbers, sets, sequences, records and mappings.
Invariants and checking: separate a property, configuration and evidence.
Resources and payment: one wallet, one attempt and an explicit completion barrier.
Objects and lifetime: two physical items, fresh occurrences and explicit references.
Priority and completion: one optional-use window and supplied completion providers.
The last three lessons use the separate payment, identity and priority packages. They are instructional specializations with their own inputs and results.
The complete selected reference profile¶
Start with Meet the reference profile. It introduces SideA and SideB and explains how the larger profile differs from the teaching models.
Zones and setup: create well-shaped objects, locations and initial context.
Turns and ending: connect phase schedules, opportunities, objectives and ending boundaries.
Object operations: distinguish moves, deployment, retirement and instruction completion.
Traversal and inspection: follow nested interaction and observation procedures.
Abilities and use: distinguish definitions, activity, triggering, payment and use.
Availability and lifetime: separate current admission, pending instances and captured authority.
Composition and assumptions: join procedures without losing caller identities or supplier obligations.
Predict one permitted change and one rejected change before following the formula. Then identify what the configured evidence actually investigates. A worked explanation helps you read a contract; its model and checking result establish a separate claim.