|
|
| Line 1: |
Line 1: |
| == Abstract view == | | == Representation invariant == |
|
| |
|
| | At any time, an object of an implementation of this abstract data structure is repesented by a positive integral number <math>N</math> and a subset <math>I</math> of <math>\{1,\ldots,N\}</math>, the '''current indexes'''. |
|
| |
|
| '''Abstract data structure:'''
| | == Method == |
| A variation of [[Sets and sequences#Maps|map]], where:
| |
| # The number of elements is bounded by some fixed positive [[Numbers#natural numbers|natural number]] <math>N</math>.
| |
| # The key type is the range <math>\{1,\ldots,N\}</math>.
| |
| # Instead of a method for inserting (key,value)-pairs, a value can be inserted alone, and the key for referring to the value is returned. As a precondition, less than <math>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 basically identical to the corresponding methods of normal maps. A key may be reused by the index handler object after removal.
| |
|
| |
|
| '''Implementation invariant:''' | | '''Name:''' reserve index |
| # There is an array <math>A</math> with index range <math>1,...,N</math>, and the component type is the value type of the map.
| |
| # There is a [[Sets and sequences|set]] <math>U</math> (for unused) of [[Numbers#natural numbers|natural numbers]].
| |
| # For each <math>i\in\{1,...,N_\text{max}\}</math> not in <math>U</math>, <math>A[i]</math> is the value associated with key <math>i</math>.
| |
|
| |
|
| == Methods ==
| | '''Precondition:''' <math>|I|<N</math>. |
|
| |
|
| | '''Return value:''' One of the indexes not in <math>I</math>. |
|
| |
|
| # The constructor takes <math>N</math> as an argument, creates <math>A</math> and <math>U</math>, and stores all potential keys <math>1,\ldots,N</math> in <math>U</math>.
| | '''Postcondition:''' The returned index is inserted in <math>I</math>. |
| # The method for inserting a new value extracts a key <math>i</math> from <math>U</math>, stores the value at <mah>A[i]</math>and returns <math>i</math>.
| | |
| # The method to look up a value for a given key <math>i</math> returns <math>A[i]</math>.
| | == Method == |
| # The method to remove a key re-inserts the key in <math>U</math>.
| | |
| | '''Name:''' release index |
Representation invariant
At any time, an object of an implementation of this abstract data structure is repesented by a positive integral number [math]\displaystyle{ N }[/math] and a subset [math]\displaystyle{ I }[/math] of [math]\displaystyle{ \{1,\ldots,N\} }[/math], the current indexes.
Method
Name: reserve index
Precondition: [math]\displaystyle{ |I|<N }[/math].
Return value: One of the indexes not in [math]\displaystyle{ I }[/math].
Postcondition: The returned index is inserted in [math]\displaystyle{ I }[/math].
Method
Name: release index