State-Machine Contracts and Failure Atomicity

What This Concept Is

An object with mutable state implements a transition system. Its public contract must describe valid inputs, returned results, permitted state changes and failed operations. A nonnegative balance invariant alone permits many incorrect accounts: one that silently discards deposits or resets to zero still keeps that invariant.

Why It Matters Here

For the lab, state is opening amount, currency and the sequence of accepted signed changes. A positive deposit appends its amount; a successful withdrawal appends its negation. Zero is accepted without an event. An insufficient withdrawal returns False and preserves every public observation. Invalid amount or currency raises ValueError, also without state change. This contract is stronger than “never negative.”

Concrete Example

Start at 10 USD minor. Withdraw 12: False, balance 10, history (). Deposit 5: None, balance 15, history (5,). Withdraw 3: True, balance 12, history (5,-3). Every prefix obeys opening + sum(history) = balance. Keep an old history snapshot after the deposit; it must remain (5,) after the withdrawal.

Common Confusion / Misconception

Validation before mutation supplies failure-state preservation for the declared sequential domain. It does not make two accounts, a database and a notification atomic. It does not handle concurrent interference or arbitrary process crashes. If publishing an event fails after a balance change, the object method needs a different consistency design; adding a class or lock-shaped comment is insufficient.

How To Use It

List each operation's input domain, result and before/after observations. Separate invalid input from valid-but-rejected requests. Check retained snapshots and an unrelated instance after each transition; then state the invariant argument.

Check Yourself

Why does a balance invariant fail to specify deposits? Which failure leaves the object unchanged, and which external effect cannot be undone by this method?

Mini Drill or Application

Give a state machine that preserves nonnegative balance yet violates deposit semantics. Write a two-call witness. Then change the contract to permit an overdraft and identify which invariant, preconditions and tests must change. Feedback: an implementation that ignores deposits keeps the invariant but fails “deposit 1; query balance.” The changed overdraft limit is a contract change, not just cleanup.

Read This Only If Stuck

Use Liskov and Wing's behavioral subtyping paper for optional formal context; the lab's finite trace checks are not a universal proof.

For an introductory account of caller guarantees, locate code contracts through the Good Code, Bad Code book index and the exact excerpt locator in the module reading guide.

Use the design contracts and labs to turn these claims into evidence.