indexing description: "Simple linear containers" author: "Patrick Schoenbach" access: cursor representation: linked contents: generic deferred class interface LINEAR_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? -- (from SEQUENCIAL_CONTAINER) 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 forth -- Move cursor forwards. require -- from SEQUENCIAL_CONTAINER not_after: not after ensure then next_position: index = old index + 1 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. require -- from SEQUENCIAL_CONTAINER not_full: not full ensure then extended: i_th (count) = v; count_increased: count = old count + 1; index_unchanged: not old empty implies index = old index put (v: G) -- Replace current item with v. require -- from SEQUENCIAL_CONTAINER not_off: not off ensure then replaced: item = v; count_unchanged: count = old count; index_unchanged: index = old index put_left (v: G) -- Insert v to the left of cursor. require -- from SEQUENCIAL_CONTAINER insertable: insertable; not_full: not full; not_before: not before ensure then inserted: i_th (index - 1) = v; count_increased: count = old count + 1; index_increased: index = old index + 1 put_right (v: G) -- Insert v to the right of cursor. require -- from SEQUENCIAL_CONTAINER insertable: insertable; not_full: not full; not_after: not after ensure then inserted: i_th (index + 1) = v; count_increased: count = old count + 1; index_unchanged: index = old index feature -- Removal remove -- Remove current item. require -- from SEQUENCIAL_CONTAINER prunable: prunable; not_empty: not empty; not_off: not off ensure then count_decreased: count = old count - 1; index_unchanged: not off implies index = old index 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); after_definition: after = (index = count + 1); before_definition: before = (index = 0); isfirst_definition: isfirst = (not empty and then (index = 1)); islast_definition: islast = (not empty and then (index = count)); -- 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 LINEAR_CONTAINER