initialization as a two-state automaton

the object has exactly two externally observable states:

• u (unprepared)
• p (prepared)

no other state is semantically visible or relevant.

a single predicate distinguishes the states:

• predicate false -> u
• predicate true -> p

the predicate must be authoritative and sufficient to decide validity for use.

• p -> p via init
• u -> u via uninit
• any transition that leaves external resources owned in u

• p implies all runtime invariants hold
• u implies no external resources are owned
• the prepared predicate is the sole authority for validity
• the prepared predicate is consistent with resource ownership
• no external resource survives a transition to u

init is atomic with respect to p:

• the object is either in u or p
• no intermediate externally visible state exists

because:

• init is total on u
• uninit returns p -> u
• failed init leaves u

the sequence:

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

is always valid.

the automaton is correct if and only if:

• all external resource ownership is confined to p
• the prepared predicate is consistent with ownership
• init and uninit are mutual inverses on observable state