Index handler

Abstract view

Abstract data structure: A variation of map, where:

The number of elements is bounded by some fixed positive natural number [math]\displaystyle{ N }[/math].
The key type is the range [math]\displaystyle{ \{1,\ldots,N\} }[/math].
Instead of a method for inserting (key,value)-pairs, a value can be inserted, and the key for referring to the value is returned. As a precondition, less than [math]\displaystyle{ N }[/math] values must be currently stored in that index handler object.
The methods to retrieve a value for a key and to remove a key and the associated value from the index handler object are identical to te correspnding metods of normal maps. A key may be reused by the index handler object after removal.

Implementation invariant:

There is an array [math]\displaystyle{ A }[/math] with index range [math]\displaystyle{ 1,...,N }[/math], and the component type is the value type of the map.
There is a set [math]\displaystyle{ U }[/math] (for unused) of natural numbers of natural numbers.
For each [math]\displaystyle{ i\in\{1,...,N_\text{max}\} }[/math] not in [math]\displaystyle{ Unused }[/math], [math]\displaystyle{ A[i] }[/math] is the value associated with key [math]\displaystyle{ i }[/math].

If an index is requested, [math]\displaystyle{ U\neq\emptyset }[/math] is a precondition. Then one index is extracted from [math]\displaystyle{ U }[/math] and returned.