Automatic generation produced by ISE Eiffel
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 interface SEQ [G -> attached ANY] create make_empty, make_from_array feature -- 2-level copy twin2: like Current feature -- Constructors make_empty -- create empty list ensure is_empty: is_empty make_from_array (a: ARRAY [G]) -- Create list from array `a'. ensure # Current = a.count across a.lower |..| a.upper as i all Current [i.item - a.lower + 1] ~ a [i.item] end feature -- Iteration new_cursor: ITERATION_CURSOR [G] -- A new cursor for iterating through current sequence feature -- Status Queries count alias "#": INTEGER_32 -- Return the number of elements in current sequence ensure Result = as_array.count Result = # as_function lower: INTEGER_32 -- Starting position of current sequence ensure Result = 1 upper: INTEGER_32 -- Ending position of current sequence ensure Result = # Current is_empty: BOOLEAN -- Is the current sequence empty? ensure Result = (# Current = 0) Result = as_array.is_empty Result = as_function.is_empty has (v: G): BOOLEAN -- Does 'v' exist in current sequence? ensure Result = across 1 |..| count as i some Current [i.item] ~ v end first: G -- Return the 1st element in current sequence require not is_empty ensure Result ~ as_array [1] Result ~ as_function [1] front: like Current -- Return current sequence except the last element require not is_empty ensure case_of_empty_init: # Current = 1 implies Result.is_empty case_of_nonempty_init: # Current > 1 implies Result ~ subsequenced (1, count - 1) last: G -- Return the last element in current sequence require not is_empty ensure Result ~ as_array [count] Result ~ as_function [count] tail: like Current -- Return current sequence except the first element require not is_empty ensure case_of_empty_tail: # Current = 1 implies Result.is_empty case_of_nonempty_tail: # Current > 1 implies Result ~ subsequenced (2, count) item alias "[]" (i: INTEGER_32): G assign override -- Element at `i'-th position require valid_position (i) ensure Result ~ as_function [i] Result ~ as_array [i] 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. 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. 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) feature -- Commands append (v: G) -- Add `v' to end. ensure Current ~ old Current.deep_twin.appended (v) prepend (v: G) -- Add `v' to beginning. ensure Current ~ old Current.deep_twin.prepended (v) subsequence (i, j: INTEGER_32) -- Cut down current seq so that segment i..j remains require valid_position (i) valid_position (j) ensure Current ~ old Current.deep_twin.subsequenced (i, j) concatenate (other: like Current) -- Append 'other' to the end of current sequence ensure Current ~ old Current.deep_twin.concatenated (other) override (v: G; i: INTEGER_32) -- Replace `i'-th entry, if in index interval, by `v'. require valid_position (i) ensure Current ~ old Current.deep_twin.overriden (v, i) 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) ensure Current ~ old Current.deep_twin.inserted (v, i) remove (i: INTEGER_32) -- Remove `i'-th entry, if in index interval require valid_position (i) ensure Current ~ old Current.deep_twin.removed (i) reverse -- Reverse the order of current sequence ensure Current ~ old Current.deep_twin.reversed feature -- Specification Queries appended alias "|->" (v: G): like Current -- Return a sequence representing current with 'v' added to end ensure current_seq_unchanged: Current ~ old Current.deep_twin count_incremented: # Result = # Current + 1 Result.front ~ Current Result.last ~ v prepended alias "|<-" (v: G): like Current -- Return a sequence representing current with 'v' added to beginning ensure current_seq_unchanged: Current ~ old Current.deep_twin count_incremented: # Result = # Current + 1 Result.first ~ v Result.tail ~ Current subsequenced (i, j: INTEGER_32): like Current -- Segment of sequence i..j require valid_position (i) valid_position (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 concatenated alias "|++|" (other: like Current): like Current -- Return a sequence representing current with 'other' appended 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 overriden (v: G; i: INTEGER_32): like Current require valid_position (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 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) ensure current_seq_unchanged: Current ~ old Current.deep_twin count_incremented: # Result = # Current + 1 Result ~ subsequenced (1, i - 1).appended (v) |++| subsequenced (i, count) 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) ensure current_seq_unchanged: Current ~ old Current.deep_twin count_decremented: # Result = # Current - 1 Result ~ subsequenced (1, i - 1) |++| subsequenced (i + 1, count) reversed: like Current -- Return an reversed version of current sequence 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 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 feature -- Quantification hold_count (exp: PREDICATE [PAIR [INTEGER_32, G]]): INTEGER_32 -- How many items satisfying `exp' are in `Current'? ensure current_seq_unchanged: Current ~ old Current.deep_twin maximum_result: Result <= count comprehension alias "|" (exp: PREDICATE [PAIR [INTEGER_32, G]]): like Current -- Form elements of current sequence that satisfy `exp' -- as a new sequence 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 feature -- Equality is_equal (other: like Current): BOOLEAN -- Is current sequence equal to `other'? ensure then Result = (as_function ~ other.as_function) feature -- Output out: STRING_8 -- Return string representation of current sequence. debug_output: STRING_8 -- Return string representation of current sequence for debugging feature -- Conversion as_array: ARRAY [G] -- Return current sequence as an array 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 as_function: FUN [INTEGER_32, G] -- Return current sequence as a function -- with its domain being the set of positions 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 feature -- Auxiliary functions for contracts valid_position (pos: INTEGER_32): BOOLEAN -- Is 'pos' a valid position in current sequence ensure Result = (1 <= pos and pos <= # Current) 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) end -- class SEQ -- Generated by ISE Eiffel --
For more details: www.eiffel.com