Section 47: State Machines and State Transition Contracts¶

TECHSPEC-47 — Section 47 · Version 0.1 · Status: Initial Draft

Status: draft. This section is an Initial Draft (Section 57 is a Working Register). It describes intended or proposed behavior, not a finalized, implemented language rule. Do not treat examples here as normative.

1. Purpose¶

Many defects occur when an object or process enters an invalid state or performs an operation in the wrong order.

State machines provide an explicit model of valid states and permitted transitions.

2. State Declaration¶

A state machine declares a finite set of named states and the transitions permitted between them.

STATE_MACHINE OrderState:
    STATE Pending
    STATE Paid
    STATE Shipped
    STATE Cancelled

The final syntax is provisional.

3. Transitions¶

Transitions declare: - Starting state. - Permitted operation. - Resulting state. - Preconditions. - Postconditions. - Effects. - Failure conditions.

Example:

TRANSITION payOrder:
    FROM Pending
    TO Paid
    REQUIRES: paymentIsAuthorized
    EFFECTS: DATABASE.MODIFY

This declaration is illustrative, not a complete executable syntax.

4. Invalid Transitions¶

An operation attempted from an undeclared state must fail explicitly.

Examples: - Shipping an unpaid order. - Paying an already cancelled order. - Cancelling an order after an irreversible shipment event, unless a separate return process is defined.

The language must not silently coerce an invalid state into a valid one.

5. State Invariants¶

Each state may have invariants that must hold whenever an object is observable in that state.

Transitions must preserve the relevant invariants.

If a transition fails partway through, the specification must define whether the state remains unchanged, enters a declared failure state, or requires recovery.

6. External Effects¶

A state transition involving a database, network service, payment processor, or other external system cannot assume atomicity across all systems.

The implementation must define: - Which effects may have occurred. - Whether the transition can be retried. - Whether compensation is available. - How uncertain outcomes are represented.

A local state rollback does not undo an external operation unless the external system confirms that reversal.

7. Concurrency¶

Concurrent transitions must be serialized or coordinated according to explicit rules.

The implementation must prevent two conflicting transitions from both being accepted based on the same stale state.

8. Verification¶

The compiler may check transition completeness, declared states, and statically detectable invalid transitions. Runtime checks may enforce state conditions. Tests and formal methods may provide additional evidence.

The existence of a state machine does not prove that every real-world workflow has been modeled correctly.

9. MVP Scope¶

State-machine syntax is deferred. The MVP can express similar rules using enums, contracts, and explicit transition functions.

10. Design Goal¶

Important state changes must be explicit, constrained, and auditable rather than scattered across unrelated conditionals.

Source and related sections¶

Source file: TECHSPEC-47.md (preserved in source-original/LANG/). See the specification index, the glossary, and the cross-reference index.