Automatic generation produced by ISE Eiffel

Classes
Clusters
Cluster hierarchy
Chart
Relations
Text
Flat
Contracts
Go to: 
note
	description: "[
		(1) Model contracts for finite sequences for elements of type G.
		(2) Queries are side effect free and return sequences via 
		    deep_twin; thus inefficient (use only for contracts).
		(3) Commands change the current sequence. 
		(4) A valid index is 1..count.
		(5) Array notation can be used, as well as iteration (across).
		(6) Empty sequences can be created, or creation can be from an array. 
		(7) Sequences have a first item (the head), a tail and last item.
		(8) Infix notation for prepended_by(x:G):
			seq1 |< x
		(9) Infix notation for appended_by(x:G):
			seq1 |> x
		(10) For concatenation may use infix: seq1 |++| seq2
		(11) For queries, to assert that the state is not changed, 
		the postcondition is
			Current ~ old Current.deep_twin
	]"
	author: "JSO"
	date: "$Date$"
	revision: "$Revision$"

class 
	SEQ [G -> attached ANY]

create 
	make_empty,
	make_from_array

feature {NONE} -- Initialization

	default_create
			-- Process instances of classes with no creation clause.
			-- (Default: do nothing.)
			-- (from ANY)
		do
		end
	
feature -- Access

	generating_type: TYPE [detachable SEQ [G]]
			-- Type of current object
			-- (type of which it is a direct instance)
			-- (from ANY)
		external
			"built_in"
		ensure -- from ANY
			generating_type_not_void: Result /= Void
		end

	generator: STRING_8
			-- Name of current object's generating class
			-- (base class of the type of which it is a direct instance)
			-- (from ANY)
		external
			"built_in"
		ensure -- from ANY
			generator_not_void: Result /= Void
			generator_not_empty: not Result.is_empty
		end
	
feature -- Comparison

	frozen deep_equal (a: detachable ANY; b: like arg #1): BOOLEAN
			-- Are `a' and `b' either both void
			-- or attached to isomorphic object structures?
			-- (from ANY)
		do
			if a = Void then
				Result := b = Void
			else
				Result := b /= Void and then a.is_deep_equal (b)
			end
		ensure -- from ANY
			shallow_implies_deep: standard_equal (a, b) implies Result
			both_or_none_void: (a = Void) implies (Result = (b = Void))
			same_type: (Result and (a /= Void)) implies (b /= Void and then a.same_type (b))
			symmetric: Result implies deep_equal (b, a)
		end

	frozen equal (a: detachable ANY; b: like arg #1): BOOLEAN
			-- Are `a' and `b' either both void or attached
			-- to objects considered equal?
			-- (from ANY)
		do
			if a = Void then
				Result := b = Void
			else
				Result := b /= Void and then a.is_equal (b)
			end
		ensure -- from ANY
			definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.is_equal (b))
		end

	frozen is_deep_equal (other: attached SEQ [G]): BOOLEAN
			-- Are `Current' and `other' attached to isomorphic object structures?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		external
			"built_in"
		ensure -- from ANY
			shallow_implies_deep: standard_is_equal (other) implies Result
			same_type: Result implies same_type (other)
			symmetric: Result implies other.is_deep_equal (Current)
		end

	frozen standard_equal (a: detachable ANY; b: like arg #1): BOOLEAN
			-- Are `a' and `b' either both void or attached to
			-- field-by-field identical objects of the same type?
			-- Always uses default object comparison criterion.
			-- (from ANY)
		do
			if a = Void then
				Result := b = Void
			else
				Result := b /= Void and then a.standard_is_equal (b)
			end
		ensure -- from ANY
			definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.standard_is_equal (b))
		end

	frozen standard_is_equal (other: attached SEQ [G]): BOOLEAN
			-- Is `other' attached to an object of the same type
			-- as current object, and field-by-field identical to it?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		external
			"built_in"
		ensure -- from ANY
			same_type: Result implies same_type (other)
			symmetric: Result implies other.standard_is_equal (Current)
		end
	
feature -- Status report

	conforms_to (other: ANY): BOOLEAN
			-- Does type of current object conform to type
			-- of `other' (as per Eiffel: The Language, chapter 13)?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		external
			"built_in"
		end

	same_type (other: ANY): BOOLEAN
			-- Is type of current object identical to type of `other'?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		external
			"built_in"
		ensure -- from ANY
			definition: Result = (conforms_to (other) and other.conforms_to (Current))
		end
	
feature -- Conversion

	as_array: ARRAY [G]
			-- Return current sequence as an array
		do
			create Result.make_empty
			across
				Current as cur
			loop
				Result.force (cur.item, Result.upper + 1)
			end
		ensure
			current_set_unchanged: Current ~ old Current.deep_twin
				Result.lower = 1
				Result.upper = count
				across
					1 |..| count as pos
				all
					Current [pos.item] ~ Result [pos.item]
				end
		end

	as_function: FUN [INTEGER_32, G]
			-- Return current sequence as a function
			-- with its domain being the set of positions
		local
			i: INTEGER_32
			pair: PAIR [INTEGER_32, G]
		do
			create Result.make_empty
			i := 1
			across
				Current as cur
			loop
				create pair.make (i, cur.item)
				Result.extend (pair)
				i := i + 1
			end
		ensure
			current_set_unchanged: Current ~ old Current.deep_twin
			all_positions_included: # Result.domain = # Current
				across
					Result.domain as pos
				all
					valid_position (pos.item)
				end
				across
					Result.domain as pos
				all
					Current [pos.item] ~ Result [pos.item]
				end
		end
	
feature -- Duplication

	frozen clone (other: detachable ANY): like other
		obsolete "Use `twin' instead."
			-- Void if `other' is void; otherwise new object
			-- equal to `other'
			--
			-- For non-void `other', clone calls copy;
			-- to change copying/cloning semantics, redefine copy.
			-- (from ANY)
		do
			if other /= Void then
				Result := other.twin
			end
		ensure -- from ANY
			equal: Result ~ other
		end

	copy (other: attached SEQ [G])
			-- Update current object using fields of object attached
			-- to `other', so as to yield equal objects.
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
			type_identity: same_type (other)
		external
			"built_in"
		ensure -- from ANY
			is_equal: Current ~ other
		end

	frozen deep_clone (other: detachable ANY): like other
		obsolete "Use `deep_twin' instead."
			-- Void if `other' is void: otherwise, new object structure
			-- recursively duplicated from the one attached to `other'
			-- (from ANY)
		do
			if other /= Void then
				Result := other.deep_twin
			end
		ensure -- from ANY
			deep_equal: deep_equal (other, Result)
		end

	frozen deep_copy (other: attached SEQ [G])
			-- Effect equivalent to that of:
			--		copy (`other' . deep_twin)
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		do
			copy (other.deep_twin)
		ensure -- from ANY
			deep_equal: deep_equal (Current, other)
		end

	frozen deep_twin: attached SEQ [G]
			-- New object structure recursively duplicated from Current.
			-- (from ANY)
		external
			"built_in"
		ensure -- from ANY
			deep_twin_not_void: Result /= Void
			deep_equal: deep_equal (Current, Result)
		end

	frozen standard_clone (other: detachable ANY): like other
		obsolete "Use `standard_twin' instead."
			-- Void if `other' is void; otherwise new object
			-- field-by-field identical to `other'.
			-- Always uses default copying semantics.
			-- (from ANY)
		do
			if other /= Void then
				Result := other.standard_twin
			end
		ensure -- from ANY
			equal: standard_equal (Result, other)
		end

	frozen standard_copy (other: attached SEQ [G])
			-- Copy every field of `other' onto corresponding field
			-- of current object.
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
			type_identity: same_type (other)
		external
			"built_in"
		ensure -- from ANY
			is_standard_equal: standard_is_equal (other)
		end

	frozen standard_twin: attached SEQ [G]
			-- New object field-by-field identical to `other'.
			-- Always uses default copying semantics.
			-- (from ANY)
		external
			"built_in"
		ensure -- from ANY
			standard_twin_not_void: Result /= Void
			equal: standard_equal (Result, Current)
		end

	frozen twin: attached SEQ [G]
			-- New object equal to `Current'
			-- twin calls copy; to change copying/twinning semantics, redefine copy.
			-- (from ANY)
		external
			"built_in"
		ensure -- from ANY
			twin_not_void: Result /= Void
			is_equal: Result ~ Current
		end
	
feature -- Basic operations

	frozen as_attached: attached SEQ [G]
			-- Attached version of Current
			-- (Can be used during transitional period to convert
			-- non-void-safe classes to void-safe ones.)
			-- (from ANY)
		do
			Result := Current
		end

	frozen default: detachable SEQ [G]
			-- Default value of object's type
			-- (from ANY)
		do
		end

	frozen default_pointer: POINTER
			-- Default value of type `POINTER'
			-- (Avoid the need to write `p'.default for
			-- some `p' of type `POINTER'.)
			-- (from ANY)
		do
		end

	default_rescue
			-- Process exception for routines with no Rescue clause.
			-- (Default: do nothing.)
			-- (from ANY)
		do
		end

	frozen do_nothing
			-- Execute a null action.
			-- (from ANY)
		do
		end
	
feature {SEQ} -- Implementation

	imp: ARRAYED_LIST [G]

	set_imp (new_imp: like imp)
		do
			imp := new_imp
		ensure
				imp = new_imp
		end
	
feature -- 2-level copy

	twin2: like Current
		do
			Result := Current.twin
			Result.set_imp (Current.imp.twin)
		end
	
feature {SEQ} -- Auxiliary functions for checking subsequences

	augmented_with_collapsed_rep: SEQ [TUPLE [g: G; i: INTEGER_32]]
			-- e.g., <<a, b, b, c, d>> augmented to
			-- <<[a, 1], [b, 2], [c, 1], [d, 1]>>
		local
			i: INTEGER_32
			element: G
		do
			create Result.make_empty
			from
				i := 1
				imp.start
			until
				imp.after
			loop
				element := imp.item
				if i > 1 then
					if imp [i - 1] ~ element then
						Result [Result.count] := [Result.last.g, Result.last.i + 1]
					else
						Result.append ([element, 1])
					end
				else
					Result.append ([element, 1])
				end
				i := i + 1
				imp.forth
			end
		end

	augmented_without_collapsed_rep: SEQ [TUPLE [G, INTEGER_32]]
			-- e.g., <<a, b, b, c, d>> augmented to
			-- <<[a, 1], [b, 1], [b, 1], [c, 1], [d, 1]>>
		do
			create Result.make_empty
			across
				Current as cur
			loop
				Result.append ([cur.item, 1])
			end
		end

	is_augmented_subseq_of (s1, s2: SEQ [TUPLE [g: G; i: INTEGER_32]]): BOOLEAN
			-- Given that both 's1' and 's2' are augmented sequences,
			-- is 's1' a contiguous subsequence of 's2'?
			-- e.g., <<[a, 1], [b, 2]>> is a contiguous subsequence of
			--       <<[a, 3], [b, 3]>>
		local
			i: INTEGER_32
		do
			if s1.is_empty then
				Result := True
			else
				from
					Result := False
					i := 1
				until
					Result or else s2.count - i + 1 < s1.count
				loop
					if s1 [1].g ~ s2 [i].g then
						Result := across
							i |..| (i + s1.count - 1) as j
						all
							s1 [j.item - i.item + 1].g ~ s2 [j.item].g and then s1 [j.item - i.item + 1].i <= s2 [j.item].i
						end
					end
					i := i + 1
				end
			end
		end
	
feature -- Auxiliary functions for contracts

	valid_position (pos: INTEGER_32): BOOLEAN
			-- Is 'pos' a valid position in current sequence
		do
			Result := 1 <= pos and then pos <= count
		ensure
				Result = (1 <= pos and pos <= # Current)
		end
	
feature -- Commands

	append (v: G)
			-- Add `v' to end.
		do
			imp.extend (v)
		ensure
				Current ~ old Current.deep_twin.appended (v)
		end

	concatenate (other: like Current)
			-- Append 'other' to the end of current sequence
		do
			across
				other as cur
			loop
				append (cur.item)
			end
		ensure
				Current ~ old Current.deep_twin.concatenated (other)
		end

	insert (v: G; i: INTEGER_32)
			-- Insert 'v' as the `i'-th entry, if in index interval
			-- e.g., insert(1) on an empty sequence is forbidden.
		require
				valid_position (i)
		local
			j: INTEGER_32
			done: BOOLEAN
		do
			from
				imp.start
				j := 1
			until
				done
			loop
				if j = i then
					imp.put_left (v)
					done := True
				end
				imp.forth
				j := j + 1
			end
		ensure
				Current ~ old Current.deep_twin.inserted (v, i)
		end

	override (v: G; i: INTEGER_32)
			-- Replace `i'-th entry, if in index interval, by `v'.
		require
				valid_position (i)
		do
			imp.put_i_th (v, i)
		ensure
				Current ~ old Current.deep_twin.overriden (v, i)
		end

	prepend (v: G)
			-- Add `v' to beginning.
		do
			imp.put_front (v)
		ensure
				Current ~ old Current.deep_twin.prepended (v)
		end

	remove (i: INTEGER_32)
			-- Remove `i'-th entry, if in index interval
		require
				valid_position (i)
		do
			imp.start
			if imp.count > 1 then
				imp.move (i - 1)
			end
			imp.remove
		ensure
				Current ~ old Current.deep_twin.removed (i)
		end

	reverse
			-- Reverse the order of current sequence
		local
			new_imp: like imp
		do
			create new_imp.make_filled (count)
			new_imp.compare_objects
			across
				1 |..| count as i
			loop
				new_imp [count - i.item + 1] := Current [i.item]
			end
			set_imp (new_imp)
		ensure
				Current ~ old Current.deep_twin.reversed
		end

	subsequence (i, j: INTEGER_32)
			-- Cut down current seq so that segment i..j remains
		require
				valid_position (i)
				valid_position (j)
		local
			pos: INTEGER_32
		do
			if i <= j then
				from
					pos := 1
					imp.start
				until
					imp.after
				loop
					if pos < i or pos > j then
						imp.remove
					else
						imp.forth
					end
					pos := pos + 1
				end
			else
				make_empty
			end
		ensure
				Current ~ old Current.deep_twin.subsequenced (i, j)
		end
	
feature -- Constructors

	make_empty
			-- create empty list
		do
			create imp.make (10)
			imp.compare_objects
		ensure
			is_empty: is_empty
		end

	make_from_array (a: ARRAY [G])
			-- Create list from array `a'.
		do
			create imp.make_from_array (a)
			imp.compare_objects
		ensure
				# Current = a.count
				across
					a.lower |..| a.upper as i
				all
					Current [i.item - a.lower + 1] ~ a [i.item]
				end
		end
	
feature -- Equality

	is_equal (other: like Current): BOOLEAN
			-- Is current sequence equal to `other'?
		require -- from ANY
			other_not_void: other /= Void
		do
			Result := imp ~ other.imp
		ensure -- from ANY
			symmetric: Result implies other ~ Current
			consistent: standard_is_equal (other) implies Result
		ensure then
				Result = (as_function ~ other.as_function)
		end
	
feature -- Iteration

	new_cursor: ITERATION_CURSOR [G]
			-- A new cursor for iterating through current sequence
		do
			Result := imp.new_cursor
		ensure -- from ITERABLE
			result_attached: Result /= Void
		end
	
feature -- Output

	debug_output: STRING_8
			-- Return string representation of current sequence for debugging
		do
			Result := out
		ensure -- from DEBUG_OUTPUT
			result_not_void: Result /= Void
		end

	Io: STD_FILES
			-- Handle to standard file setup
			-- (from ANY)
		once
			create Result
			Result.set_output_default
		ensure -- from ANY
			io_not_void: Result /= Void
		end

	out: STRING_8
			-- Return string representation of current sequence.
		local
			i: INTEGER_32
		do
			create Result.make_empty
			Result.append ("< ")
			from
				i := 1
			until
				i > count
			loop
				check
						attached {G} imp.i_th (i) as e
				then
					Result.append (e.out)
				end
				if i < count then
					Result.append (", ")
				end
				i := i + 1
			end
			Result.append (" >")
		ensure -- from ANY
			out_not_void: Result /= Void
		end

	print (o: detachable ANY)
			-- Write terse external representation of `o'
			-- on standard output.
			-- (from ANY)
		do
			if o /= Void then
				Io.put_string (o.out)
			end
		end

	frozen tagged_out: STRING_8
			-- New string containing terse printable representation
			-- of current object
			-- (from ANY)
		external
			"built_in"
		ensure -- from ANY
			tagged_out_not_void: Result /= Void
		end
	
feature -- Platform

	Operating_environment: OPERATING_ENVIRONMENT
			-- Objects available from the operating system
			-- (from ANY)
		once
			create Result
		ensure -- from ANY
			operating_environment_not_void: Result /= Void
		end
	
feature -- Quantification

	comprehension alias "|" (exp: PREDICATE [PAIR [INTEGER_32, G]]): like Current
			-- Form elements of current sequence that satisfy `exp'
			-- as a new sequence
		local
			i: INTEGER_32
			p: PAIR [INTEGER_32, G]
		do
			create Result.make_empty
			i := 1
			across
				Current as c
			loop
				create p.make (i, c.item)
				if exp.item ([p]) then
					Result.append (c.item)
				end
				i := i + 1
			end
		ensure
			current_set_unchanged: Current ~ old Current.deep_twin
			all_satisfying_items_exist: across
					Result as cur
				all
					Current.has (cur.item)
				end
			all_satisfying_exp: Result.hold_count (exp) = # Result
			consistent_satisfying_items: Current.hold_count (exp) = # Result
		end

	hold_count (exp: PREDICATE [PAIR [INTEGER_32, G]]): INTEGER_32
			-- How many items satisfying `exp' are in `Current'?
		local
			i: INTEGER_32
			p: PAIR [INTEGER_32, G]
		do
			i := 1
			across
				Current as c
			loop
				create p.make (i, c.item)
				if exp.item ([p]) then
					Result := Result + 1
				end
				i := i + 1
			end
		ensure
			current_seq_unchanged: Current ~ old Current.deep_twin
			maximum_result: Result <= count
		end
	
feature {NONE} -- Retrieval

	frozen internal_correct_mismatch
			-- Called from runtime to perform a proper dynamic dispatch on `correct_mismatch'
			-- from MISMATCH_CORRECTOR.
			-- (from ANY)
		local
			l_msg: STRING_8
			l_exc: EXCEPTIONS
		do
			if attached {MISMATCH_CORRECTOR} Current as l_corrector then
				l_corrector.correct_mismatch
			else
				create l_msg.make_from_string ("Mismatch: ")
				create l_exc
				l_msg.append (generating_type.name)
				l_exc.raise_retrieval_exception (l_msg)
			end
		end
	
feature -- Specification Queries

	appended alias "|->" (v: G): like Current
			-- Return a sequence representing current with 'v' added to end
		do
			Result := Current.deep_twin
			Result.append (v)
		ensure
			current_seq_unchanged: Current ~ old Current.deep_twin
			count_incremented: # Result = # Current + 1
				Result.front ~ Current
				Result.last ~ v
		end

	concatenated alias "|++|" (other: like Current): like Current
			-- Return a sequence representing current with 'other' appended
		do
			Result := Current.deep_twin
			Result.concatenate (other)
		ensure
			current_seq_unchanged: Current ~ old Current.deep_twin
			count_incremented: # Result = # Current + # other
				across
					1 |..| (# Current + # other) as pos
				all
					pos.item <= # Current implies Result [pos.item] ~ Current [pos.item] and pos.item > # Current implies Result [pos.item] ~ other [pos.item - # Current]
				end
		end

	inserted (v: G; i: INTEGER_32): like Current
			-- Return a new sequence representing current with
			-- `v' inserted as the `i'-th entry, if in index interval
		require
				valid_position (i)
		do
			Result := Current.deep_twin
			Result.insert (v, i)
		ensure
			current_seq_unchanged: Current ~ old Current.deep_twin
			count_incremented: # Result = # Current + 1
				Result ~ subsequenced (1, i - 1).appended (v) |++| subsequenced (i, count)
		end

	overriden (v: G; i: INTEGER_32): like Current
		require
				valid_position (i)
		do
			Result := Current.deep_twin
			Result.override (v, i)
		ensure
			current_seq_unchanged: Current ~ old Current.deep_twin
			count_incremented: # Current = # Result
				across
					1 |..| count as pos
				all
					pos.item = i implies Result [pos.item] ~ v and pos.item /= i implies Result [pos.item] ~ Current [pos.item]
				end
		end

	prepended alias "|<-" (v: G): like Current
			-- Return a sequence representing current with 'v' added to beginning
		do
			Result := Current.deep_twin
			Result.prepend (v)
		ensure
			current_seq_unchanged: Current ~ old Current.deep_twin
			count_incremented: # Result = # Current + 1
				Result.first ~ v
				Result.tail ~ Current
		end

	removed (i: INTEGER_32): like Current
			-- Return a new sequence representing current with
			-- `i'-th entry, if in index interval, removed
		require
				valid_position (i)
		do
			Result := Current.deep_twin
			Result.remove (i)
		ensure
			current_seq_unchanged: Current ~ old Current.deep_twin
			count_decremented: # Result = # Current - 1
				Result ~ subsequenced (1, i - 1) |++| subsequenced (i + 1, count)
		end

	reversed: like Current
			-- Return an reversed version of current sequence
		do
			Result := Current.deep_twin
			Result.reverse
		ensure
			current_seq_unchanged: Current ~ old Current.deep_twin
			same_count: # Current = # Result
			reverse_property_1: Current ~ Result.reversed
			reverse_property_2: across
					1 |..| count as i
				all
					Current [i.item] ~ Result [count - i.item + 1]
				end
		end

	slice (a_start, a_end, a_step: INTEGER_32): like Current
		require
				lower <= a_start and a_start <= a_end and a_end <= upper
				a_step >= 0
		local
			i: INTEGER_32
		do
			create Result.make_empty
			from
				i := a_start
			until
				i > a_end
			loop
				Result.append (item (i))
				i := i + a_step
			end
		end

	subsequenced (i, j: INTEGER_32): like Current
			-- Segment of sequence i..j
		require
				valid_position (i)
				valid_position (j)
		do
			Result := Current.deep_twin
			Result.subsequence (i, j)
		ensure
			current_seq_unchanged: Current ~ old Current.deep_twin
				j >= i implies # Result = j - i + 1
				j < i implies # Result = 0
				across
					i |..| j as pos
				all
					Current [pos.item] ~ Result [pos.item - i + 1]
				end
		end
	
feature -- Status Queries

	count alias "#": INTEGER_32
			-- Return the number of elements in current sequence
		do
			Result := imp.count
		ensure
				Result = as_array.count
				Result = # as_function
		end

	first: G
			-- Return the 1st element in current sequence
		require
				not is_empty
		do
			Result := imp [imp.Lower]
		ensure
				Result ~ as_array [1]
				Result ~ as_function [1]
		end

	front: like Current
			-- Return current sequence except the last element
		require
				not is_empty
		do
			if count > 1 then
				Result := subsequenced (1, count - 1)
			else
				create Result.make_empty
			end
		ensure
			case_of_empty_init: # Current = 1 implies Result.is_empty
			case_of_nonempty_init: # Current > 1 implies Result ~ subsequenced (1, count - 1)
		end

	has (v: G): BOOLEAN
			-- Does 'v' exist in current sequence?
		do
			Result := imp.has (v)
		ensure
				Result = across
					1 |..| count as i
				some
					Current [i.item] ~ v
				end
		end

	is_contiguous_subseq_of (other: like Current): BOOLEAN
			-- Is current a contiguous subsequence of 'other'?
			-- e.g. contiguous subsequences of <2, 3, 8, 5, 2> are:
			-- <>, <2, 3> <3, 8, 5> etc.
		do
			Result := is_augmented_subseq_of (augmented_without_collapsed_rep, other.augmented_without_collapsed_rep)
		ensure
			case_current_empty: is_empty implies Result
			case_other_empty: other.is_empty implies Result = is_empty
			case_both_non_empty: not (is_empty or other.is_empty) implies Result = (across
					1 |..| # other as start_pos
				some
					across
						1 |..| # other as end_pos
					some
						end_pos.item >= start_pos.item and Current ~ other.subsequenced (start_pos.item, end_pos.item)
					end
				end)
		end

	is_empty: BOOLEAN
			-- Is the current sequence empty?
		do
			Result := count = 0
		ensure
				Result = (# Current = 0)
				Result = as_array.is_empty
				Result = as_function.is_empty
		end

	is_subsequence_of alias "|<:" (other: like Current): BOOLEAN
			-- Is current a contiguous subsequence of 'other'?
			-- subsequences are not necessarily contiguous
			-- e.g. subsequences of <2, 3, 8, 5, 2> are:
			-- <>, <3, 5> <3, 5, 2> etc.
		local
			proj: SEQ [G]
			ran: SET [G]
			element: G
		do
			ran := Current.as_function.range
			create proj.make_empty
			across
				other as o
			loop
				element := o.item
				if ran.has (element) then
					proj.append (element)
				end
			end
			Result := is_augmented_subseq_of (augmented_with_collapsed_rep, proj.augmented_with_collapsed_rep)
		end

	item alias "[]" (i: INTEGER_32): G assign override
			-- Element at `i'-th position
		require
				valid_position (i)
		do
			Result := imp.i_th (i)
		ensure
				Result ~ as_function [i]
				Result ~ as_array [i]
		end

	last: G
			-- Return the last element in current sequence
		require
				not is_empty
		do
			Result := imp [imp.upper]
		ensure
				Result ~ as_array [count]
				Result ~ as_function [count]
		end

	lower: INTEGER_32
			-- Starting position of current sequence
		do
			Result := 1
		ensure
				Result = 1
		end

	tail: like Current
			-- Return current sequence except the first element
		require
				not is_empty
		do
			if count > 1 then
				Result := subsequenced (2, count)
			else
				create Result.make_empty
			end
		ensure
			case_of_empty_tail: # Current = 1 implies Result.is_empty
			case_of_nonempty_tail: # Current > 1 implies Result ~ subsequenced (2, count)
		end

	upper: INTEGER_32
			-- Ending position of current sequence
		do
			Result := count
		ensure
				Result = # Current
		end
	
invariant
	value_semantics: imp.object_comparison
		lower = 1
		imp.Lower = lower
		is_empty = (upper < lower)
	properties: not is_empty implies Current ~ tail.prepended (first) and Current ~ front.appended (last)

		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)

end -- class SEQ


Classes
Clusters
Cluster hierarchy
Chart
Relations
Text
Flat
Contracts
Go to: 

-- Generated by ISE Eiffel --
For more details: www.eiffel.com