Operation, Ownership, and Resource Contracts
A data structure is a contract over sequences. Specify what each operation returns, what it may change, and what every future operation may rely on. A correct final value does not establish intermediate invariants, ownership, version isolation or a resource bound.
| Field | Questions to answer |
|---|---|
| Domain | Key/value types, identity, ordering, empty and duplicate rules |
| State | Representation invariant and logical contents |
| Update | Which pointers, metadata and versions change? What is atomic in this single-threaded model? |
| Ownership | Does meld consume its donor? May versions share mutable nodes? |
| Query | Exact answer, one-sided probabilistic answer, rank convention or range convention? |
| Invalid input | Exception and guarantee that logical state is unchanged |
| Cost | Initialization, worst call, sequence/amortized, expected, numeric and output costs |
| Evidence | Independent model, invariant checker, small failing sequence and fresh transfer |
Distinct guarantees
- AVL balancing is deterministic; random insertion is not its premise.
- DSU's near-constant bound is aggregate and includes a specified initialization.
- Carry insertion's amortized heap bound requires avoiding an unconditional root scan.
- A doubling array can have a linear-cost append despite constant amortized cost.
- Skip-list/treap expectations average over internal choices under a declared model.
- Bloom no-false-negative behavior is deterministic given preserved bits and stable hashing/encoding, while its false-positive sizing formula is approximate.
- Persistent node sharing must preserve every retained version; it does not imply transactions, crash durability or concurrency safety.
Algebra of deferred updates
For the lazy sum tree, add d acts as (1,d), assign v as (0,v) in
x -> a*x+b. A length-L aggregate changes to a*S+b*L. New-after-old
composition is (a2*a1,a2*b1+b2). Identity is (1,0), not (0,0);
the latter assigns zero. These equations supply the invariant checked by
mixed operations, including queries that cause deferred tags to be pushed.
Independent state checks
The lab checker inspects AVL global bounds/heights/sizes, DSU partitions,
binomial degrees/cardinalities and live-node ownership, Fenwick block sums,
old persistent versions and untouched subtree identity. It does not simply
trust a validate() function provided by the implementation under test.
Finite stateful checks find failures but do not establish all-sequence correctness or asymptotic bounds. Prove each mutation preserves the invariant, then derive the operation cost in that invariant's reachable states.
Cost ledger and measurements
Keep units consistent. The array ledger counts element writes/copies and excludes allocation initialization. The two-stack queue example counts push and pop separately, making each transfer two primitives. Potential must use the same scale, and telescoping must retain initial potential when nonzero.
Report payload, container metadata, peak temporary allocation, retained versions, returned output and large-integer/hash work separately where relevant. A library hash call or allocation is not universally O(1). State model estimates separately from measurements, with environment, operation mix and included work.
Repair and assistance
Preserve the first failing sequence, diagnosis, invariant repair and an unseen recheck. Record book, tool or AI help and what you independently derived. Do not fabricate a quota of mistakes, infer mastery from memorized speed, or promise professional rank from passing this module.