# initialization as a two-state automaton
## state space
the object has exactly two externally observable states:
* `u` (unprepared)
* `p` (prepared)

no other state is semantically visible or relevant.

## state predicate
a single predicate distinguishes the states:
* predicate false -> `u`
* predicate true  -> `p`

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

## transitions
### init
`u` -> `p`

obligations:
* acquire all required external resources
* authoritatively write all runtime-relevant state
* set the prepared predicate

failure rule:
* on failure, release all acquired external resources
* leave predicate false
* state remains `u`

init is total on `u`.

### uninit
`p` -> `u`

obligations:
* release all external resources owned by the object
* clear the prepared predicate

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
* any transition that leaves external resources owned in `u`

## invariants
* `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`

## atomicity invariant
init is atomic with respect to `p`:
* the object is either in `u` or `p`
* no intermediate externally visible state exists

## reinitialization guarantee
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.

## minimal correctness criterion
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