2026-02-24

initialization as a two-state automaton

state space

the object has exactly two states:

u (unprepared)
p (prepared)

no other state is semantically relevant.

semantic vs representation state

semantic state is defined only by successful transitions and external resource ownership.

representation state is the concrete byte contents of the object.

the automaton constrains semantic state only.

state definition

state is determined by successful transitions:

before any successful init -> u
after a successful init and before uninit -> p
after uninit -> u

failed init attempts are not transitions.

transitions

init

u -> p

obligations:

acquire all required external resources
authoritatively write all runtime-relevant state
establish all runtime invariants

obligations on failure:

leave the object owning no external resources
ensure another init call on the same object is valid

init is total on u.

uninit

p -> u

obligations:

release all external resources owned by the object

non-obligations:

no requirement to zero fields
no requirement to restore configuration templates
no requirement to repair non-owning internal references

uninit is total on p.

forbidden transitions

p -> p via init
u -> u via uninit
calling uninit before a successful init
any transition that leaves external resources owned in u

invariants

p implies all runtime invariants hold
u implies no external resources are owned
no external resource survives a transition to u
representation state in u is unconstrained except that init is permitted

atomicity invariant

init is atomic with respect to semantic state at function return:

upon return, the object is either in u or p
partial resource acquisition during execution is permitted
on failure return, no external resources remain owned

reinitialization guarantee

because:

init is total on u
uninit returns p -> u
failed init leaves the object in u

the sequence:

`u` -> init -> `p` -> uninit -> `u` -> init -> ...

is always valid.

minimal correctness criterion

the automaton is correct if and only if:

all external resource ownership is confined to p
failed init leaves the object in u and permits another init
init and uninit are mutual inverses on semantic state

Addendum

Any external resource whose ownership would characterize the p state (being a property of it) should, from the moment of acquisition, be represented in the object. No such direct ownership may be staged or duplicated in locals for later publication.

On failure return from init, the implementation performs only the releases necessary to ensure that the object owns no external resources. It performs no additional representation writes for restoration, normalization, or repair.

init is defined to operate correctly on any representation satisfying the u invariant, independent of its byte contents. The sole semantic requirement on failure is therefore: no external resources remain owned.