indexing description: "Container with bidirectional sequencial access" names: sequencial, bidirectional access: cursor author: "Patrick Schoenbach" deferred class interface TWO_WAY_SEQUENCIAL_CONTAINER [G] feature -- Access i_th (i: INTEGER): G -- i-th item -- (from SEQUENCIAL_CONTAINER) require -- from SEQUENCIAL_CONTAINER valid_index: valid_index (i) index: INTEGER -- Current index -- (from SEQUENCIAL_CONTAINER) item: G -- Current item -- (from SEQUENCIAL_CONTAINER) require -- from SEQUENCIAL_CONTAINER not_off: not off feature -- Measurement capacity: INTEGER -- Size of container -- (from SEQUENCIAL_CONTAINER) count: INTEGER -- Number of elements -- (from SEQUENCIAL_CONTAINER) feature -- Status report after: BOOLEAN -- Is there no valid cursor position to the right of cursor? -- (from SEQUENCIAL_CONTAINER) before: BOOLEAN -- Is there no valid cursor position to the left of cursor? empty: BOOLEAN -- Is container empty? -- (from SEQUENCIAL_CONTAINER) full: BOOLEAN -- Is container full? -- (from SEQUENCIAL_CONTAINER) insertable: BOOLEAN -- Can elements be inserted in the middle? -- (from SEQUENCIAL_CONTAINER) isfirst: BOOLEAN -- Is cursor on first element? -- (from SEQUENCIAL_CONTAINER) islast: BOOLEAN -- Is cursor on last element? -- (from SEQUENCIAL_CONTAINER) off: BOOLEAN -- Is there no current item? -- (from SEQUENCIAL_CONTAINER) prunable: BOOLEAN -- Is container prunable? -- (from SEQUENCIAL_CONTAINER) resizable: BOOLEAN -- Is container resizable? -- (from SEQUENCIAL_CONTAINER) valid_index (i: INTEGER): BOOLEAN -- Is index i valid? -- (from SEQUENCIAL_CONTAINER) feature -- Cursor movement back -- Move cursor backwards. require not_before: not before finish -- Move cursor to last element. require not_empty: not empty ensure cursor_at_end: islast forth -- Move cursor forwards. -- (from SEQUENCIAL_CONTAINER) require -- from SEQUENCIAL_CONTAINER not_after: not after go_i_th (i: INTEGER) -- Move cursor to the i-th position. -- (from SEQUENCIAL_CONTAINER) require -- from SEQUENCIAL_CONTAINER valid_index: valid_index (i) ensure -- from SEQUENCIAL_CONTAINER i_th_position: index = i start -- Move cursor to first element. -- (from SEQUENCIAL_CONTAINER) require -- from SEQUENCIAL_CONTAINER not_empty: not empty ensure -- from SEQUENCIAL_CONTAINER cursor_at_start: isfirst feature -- Element change extend (v: G) -- Add v to the end of structure. -- (from SEQUENCIAL_CONTAINER) require -- from SEQUENCIAL_CONTAINER not_full: not full put (v: G) -- Replace current item with v. -- (from SEQUENCIAL_CONTAINER) require -- from SEQUENCIAL_CONTAINER not_off: not off put_left (v: G) -- Insert v to the right of cursor. -- (from SEQUENCIAL_CONTAINER) require -- from SEQUENCIAL_CONTAINER insertable: insertable; not_full: not full; not_before: not before put_right (v: G) -- Insert v to the right of cursor. -- (from SEQUENCIAL_CONTAINER) require -- from SEQUENCIAL_CONTAINER insertable: insertable; not_full: not full; not_after: not after feature -- Removal remove -- Remove current item. -- (from SEQUENCIAL_CONTAINER) require -- from SEQUENCIAL_CONTAINER prunable: prunable; not_empty: not empty; not_off: not off wipe_out -- Empty container. -- (from SEQUENCIAL_CONTAINER) ensure -- from SEQUENCIAL_CONTAINER empty: empty feature -- Resizing resize (n: INTEGER) -- Resize container to n elements. -- (from SEQUENCIAL_CONTAINER) require -- from SEQUENCIAL_CONTAINER resizable: resizable; size_increasing: n > capacity ensure -- from SEQUENCIAL_CONTAINER resized: capacity = n invariant -- from GENERAL reflexive_equality: standard_is_equal (Current); reflexive_conformance: conforms_to (Current); off_definition: off = (before or after); -- from SEQUENCIAL_CONTAINER empty_definition: empty = (count = 0); off_definition: off = (before or after); empty_constraint: empty implies off; count_range: 0 <= count and count <= capacity; end -- class TWO_WAY_SEQUENCIAL_CONTAINER