SQL_SCAN Flat contracts

indexing
status: "See notice at end of class"
date: "$Date$"
revision: "$Revision$"
product: "EiffelStore"

class interface
SQL_SCAN

create

make (i: INTEGER)
-- Create format and allocate string.

feature -- Initialization

adapt (s: STRING): like Current
-- Object of a type conforming to the type of s,
-- initialized with attributes from s
-- (from STRING)

from_c (c_string: POINTER)
-- Reset contents of string from contents of c_string,
-- a string created by some external C function.
-- (from STRING)
require -- from STRING
c_string_exists: c_string /= default_pointer
ensure -- from STRING
no_zero_byte: not has ('%U')

from_c_substring (c_string: POINTER; start_pos, end_pos: INTEGER)
-- Reset contents of string from substring of c_string,
-- a string created by some external C function.
-- (from STRING)
require -- from STRING
c_string_exists: c_string /= default_pointer
start_position_big_enough: start_pos >= 1
end_position_big_enough: start_pos <= end_pos + 1
ensure -- from STRING
valid_count: count = end_pos - start_pos + 1

make (i: INTEGER)
-- Create format and allocate string.

format_make
-- Create an interface object to format data.
-- (from DB_FORMAT)

make_from_c (c_string: POINTER)
-- Initialize from contents of c_string,
-- a string created by some external C function
-- (from STRING)
require -- from STRING
c_string_exists: c_string /= default_pointer

make_from_string (s: STRING)
-- Initialize from the characters of s.
-- (Useful in proper descendants of class STRING,
-- to initialize a string-like object from a manifest string.)
-- (from STRING)
require -- from STRING
string_exists: s /= void
ensure -- from STRING
shared_implementation: shared_with (s)

remake (n: INTEGER)
-- Allocate space for at least n characters.
-- (from STRING)
require -- from STRING
non_negative_size: n >= 0
ensure -- from STRING
empty_string: count = 0
area_allocated: capacity >= n

feature -- Access

area: SPECIAL [CHARACTER]
-- Special data zone
-- (from TO_SPECIAL)

Bit_type: INTEGER is 8
-- (from INTERNAL)

boolean_field (i: INTEGER; object: ANY): BOOLEAN
-- Boolean value of i-th field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
boolean_field: field_type (i, object) = boolean_type

Boolean_type: INTEGER is 3
-- (from INTERNAL)

character_field (i: INTEGER; object: ANY): CHARACTER
-- Character value of i-th field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
character_field: field_type (i, object) = character_type

Character_type: INTEGER is 2
-- (from INTERNAL)

class_name (object: ANY): STRING
-- Name of the class associated with object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void

double_field (i: INTEGER; object: ANY): DOUBLE
-- Double precision value of i-th field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
double_field: field_type (i, object) = double_type

Double_type: INTEGER is 6
-- (from INTERNAL)

dynamic_type (object: ANY): INTEGER
-- Dynamic type of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void

expanded_field_type (i: INTEGER; object: ANY): STRING
-- Class name associated with the i-th
-- expanded field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
is_expanded: field_type (i, object) = expanded_type
ensure -- from INTERNAL
result_exists: Result /= void

Expanded_type: INTEGER is 7
-- (from INTERNAL)

False_constant: STRING is "false"
-- Constant string "false"
-- (from STRING)

field (i: INTEGER; object: ANY): ANY
-- Object attached to the i-th field of object
-- (directly or through a reference)
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
not_special: not is_special (object)

field_name (i: INTEGER; object: ANY): STRING
-- Name of i-th field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
not_special: not is_special (object)
ensure -- from INTERNAL
result_exists: Result /= void

field_offset (i: INTEGER; object: ANY): INTEGER
-- Offset of i-th field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
not_special: not is_special (object)

field_type (i: INTEGER; object: ANY): INTEGER
-- Type of i-th field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)

fuzzy_index (other: STRING; start: INTEGER; fuzz: INTEGER): INTEGER
-- Position of first occurrence of other at or after start
-- with 0..fuzz mismatches between the string and other.
-- 0 if there are no fuzzy matches
-- (from STRING)
require -- from STRING
other_exists: other /= void
other_not_empty: not other.is_empty
start_large_enough: start >= 1
start_small_enough: start <= count
acceptable_fuzzy: fuzz <= other.count

generic_dynamic_type (object: ANY; i: INTEGER): INTEGER
-- Dynamic type of generic parameter of object at
-- position i.
-- (from INTERNAL)

has (c: CHARACTER): BOOLEAN
-- Does string include c?
-- (from STRING)
ensure -- from CONTAINER
not_found_in_empty: Result implies not is_empty

hash_code: INTEGER
-- Hash code value
-- (from STRING)
ensure -- from HASHABLE
good_hash_value: Result >= 0

index_of (c: CHARACTER; start: INTEGER): INTEGER
-- Position of first occurrence of c at or after start;
-- 0 if none.
-- (from STRING)
require -- from STRING
start_large_enough: start >= 1
start_small_enough: start <= count + 1
ensure -- from STRING
correct_place: Result > 0 implies item (Result) = c

Integer_16_type: INTEGER is 10
-- (from INTERNAL)

Integer_32_type: INTEGER is 4
-- (from INTERNAL)

Integer_64_type: INTEGER is 11
-- (from INTERNAL)

Integer_8_type: INTEGER is 9
-- (from INTERNAL)

integer_field (i: INTEGER; object: ANY): INTEGER
-- Integer value of i-th field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
integer_field: field_type (i, object) = integer_type

Integer_type: INTEGER is 4
-- (from INTERNAL)

item (i: INTEGER): CHARACTER
-- Character at position i
-- Was declared in STRING as synonym of @.
-- (from STRING)
require -- from TABLE
valid_key: valid_index (k)

item_code (i: INTEGER): INTEGER
-- Numeric code of character at position i
-- (from STRING)
require -- from STRING
index_small_enough: i <= count
index_large_enough: i > 0

last_index_of (c: CHARACTER; start_index_from_end: INTEGER): INTEGER
-- Position of last occurence of c.
-- 0 if none
-- (from STRING)
require -- from STRING
start_index_small_enough: start_index_from_end <= count
start_index_large_enough: start_index_from_end >= 1
ensure -- from STRING
correct_place: Result > 0 implies item (Result) = c

pointer_field (i: INTEGER; object: ANY): POINTER
-- Pointer value of i-th field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
pointer_field: field_type (i, object) = pointer_type

Pointer_type: INTEGER is 0
-- (from INTERNAL)

real_field (i: INTEGER; object: ANY): REAL
-- Real value of i-th field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
real_field: field_type (i, object) = real_type

Real_type: INTEGER is 5
-- (from INTERNAL)

Reference_type: INTEGER is 1
-- (from INTERNAL)

shared_with (other: like Current): BOOLEAN
-- Does string share the text of other?
-- (from STRING)

substring_index (other: STRING; start: INTEGER): INTEGER
-- Position of first occurrence of other at or after start;
-- 0 if none.
-- (from STRING)
require -- from STRING
other_nonvoid: other /= void
other_notempty: not other.is_empty
start_large_enough: start >= 1
start_small_enough: start <= count
ensure -- from STRING
correct_place: Result > 0 implies substring (Result, Result + other.count - 1).is_equal (other)

True_constant: STRING is "true"
-- Constant string "true"
-- (from STRING)

Wide_character_type: INTEGER is 12
-- (from INTERNAL)

infix "@" (i: INTEGER): CHARACTER
-- Character at position i
-- Was declared in STRING as synonym of item.
-- (from STRING)
require -- from TABLE
valid_key: valid_index (k)

feature -- Measurement

additional_space: INTEGER
-- Proposed number of additional items
-- (from RESIZABLE)
ensure -- from RESIZABLE
at_least_one: Result >= 1

bit_size (i: INTEGER; object: ANY): INTEGER
-- Size (in bit) of the i-th bit field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
is_bit: field_type (i, object) = bit_type
ensure -- from INTERNAL
positive_result: Result > 0

capacity: INTEGER
-- Allocated space
-- (from STRING)

count: INTEGER
-- Actual number of characters making up the string
-- (from STRING)

field_count (object: ANY): INTEGER
-- Number of logical fields in object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void

Growth_percentage: INTEGER is 50
-- Percentage by which structure will grow automatically
-- (from RESIZABLE)

index_set: INTEGER_INTERVAL
-- Range of acceptable indexes
-- (from STRING)
ensure -- from INDEXABLE
not_void: Result /= void
ensure then -- from STRING
Result.count = count

Minimal_increase: INTEGER is 5
-- Minimal number of additional items
-- (from RESIZABLE)

occurrences (c: CHARACTER): INTEGER
-- Number of times c appears in the string
-- (from STRING)
ensure -- from BAG
non_negative_occurrences: Result >= 0

physical_size (object: ANY): INTEGER
-- Space occupied by object in bytes
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void

feature -- Comparison

is_equal (other: like Current): BOOLEAN
-- Is string made of same character sequence as other
-- (possibly with a different capacity)?
-- (from STRING)
require -- from ANY
other_not_void: other /= void
ensure -- from ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
ensure then -- from COMPARABLE
trichotomy: Result = (not (Current < other) and not (other < Current))

max (other: like Current): like Current
-- The greater of current object and other
-- (from COMPARABLE)
require -- from COMPARABLE
other_exists: other /= void
ensure -- from COMPARABLE
current_if_not_smaller: Current >= other implies Result = Current
other_if_smaller: Current < other implies Result = other

min (other: like Current): like Current
-- The smaller of current object and other
-- (from COMPARABLE)
require -- from COMPARABLE
other_exists: other /= void
ensure -- from COMPARABLE
current_if_not_greater: Current <= other implies Result = Current
other_if_greater: Current > other implies Result = other

three_way_comparison (other: like Current): INTEGER
-- If current object equal to other, 0;
-- if smaller, -1; if greater, 1
-- (from COMPARABLE)
require -- from COMPARABLE
other_exists: other /= void
ensure -- from COMPARABLE
equal_zero: (Result = 0) = is_equal (other)
smaller_negative: (Result = - 1) = (Current < other)
greater_positive: (Result = 1) = (Current > other)

infix "<" (other: like Current): BOOLEAN
-- Is string lexicographically lower than other?
-- (from STRING)
require -- from PART_COMPARABLE
other_exists: other /= void
ensure then -- from COMPARABLE
asymmetric: Result implies not (other < Current)

infix "<=" (other: like Current): BOOLEAN
-- Is current object less than or equal to other?
-- (from COMPARABLE)
require -- from PART_COMPARABLE
other_exists: other /= void
ensure then -- from COMPARABLE
definition: Result = ((Current < other) or is_equal (other))

infix ">" (other: like Current): BOOLEAN
-- Is current object greater than other?
-- (from COMPARABLE)
require -- from PART_COMPARABLE
other_exists: other /= void
ensure then -- from COMPARABLE
definition: Result = (other < Current)

infix ">=" (other: like Current): BOOLEAN
-- Is current object greater than or equal to other?
-- (from COMPARABLE)
require -- from PART_COMPARABLE
other_exists: other /= void
ensure then -- from COMPARABLE
definition: Result = (other <= Current)

feature -- Status report

Changeable_comparison_criterion: BOOLEAN is False
-- (from STRING)

Extendible: BOOLEAN is True
-- May new items be added? (Answer: yes.)
-- (from STRING)

full: BOOLEAN
-- Is structure full?
-- (from BOUNDED)

string_is_boolean: BOOLEAN
-- Does Current represent a BOOLEAN?
-- (from STRING)

string_is_double: BOOLEAN
-- Does Current represent a DOUBLE?
-- (from STRING)

is_empty: BOOLEAN
-- Is structure empty?
-- (from FINITE)

is_hashable: BOOLEAN
-- May current object be hashed?
-- (True if it is not its type's default.)
-- (from HASHABLE)
ensure -- from HASHABLE
ok_if_not_default: Result implies (Current /= default)

is_inserted (v: CHARACTER): BOOLEAN
-- Has v been inserted by the most recent insertion?
-- (By default, the value returned is equivalent to calling
-- `has (v)'. However, descendants might be able to provide more
-- efficient implementations.)
-- (from COLLECTION)

string_is_integer: BOOLEAN
-- Does Current represent an INTEGER?
-- (from STRING)

is_mapped (key: STRING): BOOLEAN
-- Is key mapped to an Eiffel entity?
-- (from STRING_HDL)
require -- from STRING_HDL
keys_exists: key /= void

string_is_real: BOOLEAN
-- Does Current represent a REAL?
-- (from STRING)

is_special (object: ANY): BOOLEAN
-- Is object a special object?
-- It only recognized a special object
-- initialized within a TO_SPECIAL object.
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void

mapped_value (key: STRING): ANY
-- Value mapped with key
-- (from STRING_HDL)
require -- from STRING_HDL
key_exists: key /= void
key_mapped: is_mapped (key)
ensure -- from STRING_HDL
result_exists: Result /= void

object_comparison: BOOLEAN
-- Must search operations use equal rather than =
-- for comparing references? (Default: no, use =.)
-- (from CONTAINER)

prunable: BOOLEAN
-- May items be removed? (Answer: yes.)
-- (from STRING)

resizable: BOOLEAN
-- May capacity be changed? (Answer: yes.)
-- (from RESIZABLE)

valid_index (i: INTEGER): BOOLEAN
-- Is i within the bounds of the string?
-- (from STRING)
ensure then -- from INDEXABLE
only_if_in_index_set: Result implies ((i >= index_set.lower) and (i <= index_set.upper))

feature -- Status setting

clear_all
-- Remove all mapped keys.
-- (from STRING_HDL)
ensure -- from STRING
is_empty: count = 0
same_capacity: capacity = old capacity

compare_objects
-- Ensure that future search operations will use equal
-- rather than = for comparing references.
-- (from CONTAINER)
require -- from CONTAINER
changeable_comparison_criterion
ensure -- from CONTAINER
object_comparison

compare_references
-- Ensure that future search operations will use =
-- rather than equal for comparing references.
-- (from CONTAINER)
require -- from CONTAINER
changeable_comparison_criterion
ensure -- from CONTAINER
reference_comparison: not object_comparison

set_map_name (n: ANY; key: STRING)
-- Store item n with key key.
-- n can be Void.
-- (from STRING_HDL)
require -- from STRING_HDL
key_exists: key /= void
not_key_in_table: not is_mapped (key)
ensure -- from STRING_HDL
ht.count = old ht.count + 1

unset_map_name (key: STRING)
-- Remove item associated with key key.
-- (from STRING_HDL)
require -- from STRING_HDL
key_exists: key /= void
item_exists: is_mapped (key)
ensure -- from STRING_HDL
ht.count = old ht.count - 1

feature -- Element change

append (s: STRING)
-- Append a copy of s at end.
-- (from STRING)
require -- from STRING
argument_not_void: s /= void
ensure -- from STRING
new_count: count = old count + old s.count

append_boolean (b: BOOLEAN)
-- Append the string representation of b at end.
-- (from STRING)

append_character (c: CHARACTER)
-- Append c at end.
-- Was declared in STRING as synonym of extend.
-- (from STRING)
ensure then -- from STRING
item_inserted: item (count) = c
new_count: count = old count + 1

append_double (d: DOUBLE)
-- Append the string representation of d at end.
-- (from STRING)

append_integer (i: INTEGER)
-- Append the string representation of i at end.
-- (from STRING)

append_real (r: REAL)
-- Append the string representation of r at end.
-- (from STRING)

append_string (s: STRING)
-- Append a copy of s, if not void, at end.
-- (from STRING)

copy (other: like Current)
-- Reinitialize by copying the characters of other.
-- (This is also used by clone.)
-- (from STRING)
require -- from ANY
other_not_void: other /= void
type_identity: same_type (other)
ensure -- from ANY
is_equal: is_equal (other)
ensure then -- from STRING
new_result_count: count = other.count

extend (c: CHARACTER)
-- Append c at end.
-- Was declared in STRING as synonym of append_character.
-- (from STRING)
require -- from COLLECTION
extendible: extendible
ensure -- from COLLECTION
item_inserted: is_inserted (v)
ensure then -- from BAG
one_more_occurrence: occurrences (v) = old (occurrences (v)) + 1
ensure then -- from STRING
item_inserted: item (count) = c
new_count: count = old count + 1

fill (other: CONTAINER [CHARACTER])
-- Fill with as many items of other as possible.
-- The representations of other and current structure
-- need not be the same.
-- (from COLLECTION)
require -- from COLLECTION
other_not_void: other /= void
extendible

fill_blank
-- Fill with capacity blank characters.
-- (from STRING)
ensure -- from STRING
filled: full
same_size: (count = capacity) and (capacity = old capacity)

fill_character (c: CHARACTER)
-- Fill with capacity characters all equal to c.
-- (from STRING)
ensure -- from STRING
filled: full
same_size: (count = capacity) and (capacity = old capacity)

head (n: INTEGER)
-- Remove all characters except for the first n;
-- do nothing if n >= count.
-- (from STRING)
require -- from STRING
non_negative_argument: n >= 0
ensure -- from STRING
new_count: count = n.min (old count)

insert (s: STRING; i: INTEGER)
-- Add s to the left of position i in current string.
-- (from STRING)
require -- from STRING
string_exists: s /= void
index_small_enough: i <= count
index_large_enough: i > 0
ensure -- from STRING
new_count: count = old count + s.count

left_adjust
-- Remove leading whitespace.
-- (from STRING)
ensure -- from STRING
new_count: (count /= 0) implies ((item (1) /= ' ') and (item (1) /= '   ') and (item (1) /= '%R') and (item (1) /= ''))

precede (c: CHARACTER)
-- Add c at front.
-- (from STRING)
ensure -- from STRING
new_count: count = old count + 1

prepend (s: STRING)
-- Prepend a copy of s at front.
-- (from STRING)
require -- from STRING
argument_not_void: s /= void
ensure -- from STRING
new_count: count = old count + s.count

prepend_boolean (b: BOOLEAN)
-- Prepend the string representation of b at front.
-- (from STRING)

prepend_character (c: CHARACTER)
-- Prepend the string representation of c at front.
-- (from STRING)

prepend_double (d: DOUBLE)
-- Prepend the string representation of d at front.
-- (from STRING)

prepend_integer (i: INTEGER)
-- Prepend the string representation of i at front.
-- (from STRING)

prepend_real (r: REAL)
-- Prepend the string representation of r at front.
-- (from STRING)

prepend_string (s: STRING)
-- Prepend a copy of s, if not void, at front.
-- (from STRING)

put (c: CHARACTER; i: INTEGER)
-- Replace character at position i by c.
-- (from STRING)
require -- from TABLE
valid_key: valid_index (k)
ensure then -- from INDEXABLE
insertion_done: item (k) = v

replace_blank
-- Replace all current characters with blanks.
-- (from STRING)
ensure -- from STRING
same_size: (count = old count) and (capacity = old capacity)

replace_character (c: CHARACTER)
-- Replace all current characters with characters all equal to c.
-- (from STRING)
ensure -- from STRING
same_size: (count = old count) and (capacity = old capacity)

replace_substring (s: like Current; start_pos, end_pos: INTEGER)
-- Copy the characters of s to positions
-- start_pos .. end_pos.
-- (from STRING)
require -- from STRING
string_exists: s /= void
index_small_enough: end_pos <= count
order_respected: start_pos <= end_pos
index_large_enough: start_pos > 0
ensure -- from STRING
new_count: count = old count + s.count - end_pos + start_pos - 1

replace_substring_all (original, new: like Current)
-- Replace every occurence of original with new.
-- (from STRING)
require -- from STRING
original_exists: original /= void
new_exists: new /= void
original_not_empty: not original.is_empty

right_adjust
-- Remove trailing whitespace.
-- (from STRING)
ensure -- from STRING
new_count: (count /= 0) implies ((item (count) /= ' ') and (item (count) /= '   ') and (item (count) /= '%R') and (item (count) /= ''))

set (t: like Current; n1, n2: INTEGER)
-- Set current string to substring of t from indices n1
-- to n2, or to empty string if no such substring.
-- (from STRING)
require -- from STRING
argument_not_void: t /= void
ensure -- from STRING
is_substring: is_equal (t.substring (n1, n2))

set_boolean_field (i: INTEGER; object: ANY; value: BOOLEAN)
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
boolean_field: field_type (i, object) = boolean_type

set_character_field (i: INTEGER; object: ANY; value: CHARACTER)
-- Set character value of i-th field of object to value
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
character_field: field_type (i, object) = character_type

set_double_field (i: INTEGER; object: ANY; value: DOUBLE)
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
double_field: field_type (i, object) = double_type

set_integer_field (i: INTEGER; object: ANY; value: INTEGER)
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
integer_field: field_type (i, object) = integer_type

set_pointer_field (i: INTEGER; object: ANY; value: POINTER)
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
pointer_field: field_type (i, object) = pointer_type

set_real_field (i: INTEGER; object: ANY; value: REAL)
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
real_field: field_type (i, object) = real_type

set_reference_field (i: INTEGER; object: ANY; value: ANY)
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
reference_field: field_type (i, object) = reference_type

share (other: like Current)
-- Make current string share the text of other.
-- Subsequent changes to the characters of current string
-- will also affect other, and conversely.
-- (from STRING)
require -- from STRING
argument_not_void: other /= void
ensure -- from STRING
shared_count: other.count = count

subcopy (other: like Current; start_pos, end_pos, index_pos: INTEGER)
-- Copy characters of other within bounds start_pos and
-- end_pos to current string starting at index index_pos.
-- (from STRING)
require -- from STRING
other_not_void: other /= void
valid_start_pos: other.valid_index (start_pos)
valid_end_pos: other.valid_index (end_pos)
valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1)
valid_index_pos: valid_index (index_pos)
enough_space: (count - index_pos) >= (end_pos - start_pos)

tail (n: INTEGER)
-- Remove all characters except for the last n;
-- do nothing if n >= count.
-- (from STRING)
require -- from STRING
non_negative_argument: n >= 0
ensure -- from STRING
new_count: count = n.min (old count)

infix "+" (s: STRING): STRING
-- Append a copy of 's' at the end of a copy of Current,
-- Then return the Result.
-- (from STRING)
require -- from STRING
argument_not_void: s /= void
ensure -- from STRING
result_exists: Result /= void
new_count: Result.count = count + s.count

feature -- Removal

prune (c: CHARACTER)
-- Remove first occurrence of c, if any.
-- (from STRING)
require -- from COLLECTION
prunable: prunable
require else -- from STRING
True

prune_all (c: CHARACTER)
-- Remove all occurrences of c.
-- (from STRING)
require -- from COLLECTION
prunable
require else -- from STRING
True
ensure -- from COLLECTION
no_more_occurrences: not has (v)
ensure then -- from STRING
changed_count: count = (old count) - (old occurrences (c))

prune_all_leading (c: CHARACTER)
-- Remove all leading occurrences of c.
-- (from STRING)

prune_all_trailing (c: CHARACTER)
-- Remove all trailing occurrences of c.
-- (from STRING)

remove (i: INTEGER)
-- Remove i-th character.
-- (from STRING)
require -- from STRING
index_small_enough: i <= count
index_large_enough: i > 0
ensure -- from STRING
new_count: count = old count - 1

wipe_out
-- Remove all characters.
-- (from STRING)
require -- from COLLECTION
prunable
ensure -- from COLLECTION
wiped_out: is_empty
ensure then -- from STRING
is_empty: count = 0
empty_capacity: capacity = 0

feature -- Resizing

adapt_size
-- Adapt the size to accommodate count characters.
-- (from STRING)

automatic_grow
-- Change the capacity to accommodate at least
-- Growth_percentage more items.
-- (from RESIZABLE)
ensure -- from RESIZABLE
increased_capacity: capacity >= old capacity + old capacity * growth_percentage // 100

grow (newsize: INTEGER)
-- Ensure that the capacity is at least newsize.
-- (from STRING)
require -- from RESIZABLE
True
require else -- from STRING
new_size_non_negative: newsize >= 0
ensure -- from RESIZABLE
new_capacity: capacity >= i

resize (newsize: INTEGER)
-- Rearrange string so that it can accommodate
-- at least newsize characters.
-- Do not lose any previously entered character.
-- (from STRING)
require -- from STRING
new_size_non_negative: newsize >= 0

feature -- Conversion

boolean_format (object: BOOLEAN): STRING
-- Converted string of object according to the database format
-- (from DB_FORMAT)

center_justify
-- Center justify the string using
-- the capacity as the width
-- (from STRING)

character_justify (pivot: CHARACTER; position: INTEGER)
-- Justify a string based on a pivot
-- and the position it needs to be in
-- the final string.
-- This will grow the string if necessary
-- to get the pivot in the correct place.
-- (from STRING)
require -- from STRING
valid_position: position <= capacity
positive_position: position >= 1
pivot_not_space: pivot /= ' '
not_empty: not is_empty

charconv (i: INTEGER): CHARACTER
-- Character corresponding to ascii code i
-- (from BASIC_ROUTINES)

date_format (object: DATE_TIME): STRING
-- Converted string of object according to the database format.
-- (from DB_FORMAT)
require -- from DB_FORMAT
argument_not_void: object /= void

left_justify
-- Left justify the string using
-- the capacity as the width
-- (from STRING)

linear_representation: LINEAR [CHARACTER]
-- Representation as a linear structure
-- (from STRING)

mirror
-- Reverse the order of characters.
-- "Hello world" -> "dlrow olleH".
-- (from STRING)
ensure -- from STRING
same_count: count = old count

mirrored: like Current
-- Mirror image of string;
-- result for "Hello world" is "dlrow olleH".
-- (from STRING)
ensure -- from STRING
same_count: Result.count = count

right_justify
-- Right justify the string using
-- the capacity as the width
-- (from STRING)

split (a_separator: CHARACTER): LINEAR [STRING]
-- Split on a_separator.
-- Ignore separators in quotes.
-- (from STRING)
ensure -- from STRING
Result /= void

string_format (object: STRING): STRING
-- Converted string of object according to the database format.
-- (from DB_FORMAT)
require -- from DB_FORMAT
argument_not_void: object /= void

to_boolean: BOOLEAN
-- Boolean value;
-- "True" yields True, "False" yields False
-- (case-insensitive)
-- (from STRING)
require -- from STRING
is_boolean: string_is_boolean

frozen to_c: ANY
-- A reference to a C form of current string.
-- Useful only for interfacing with C software.
-- (from STRING)

to_double: DOUBLE
-- "Double" value;
-- for example, when applied to "123.0", will yield 123.0 (double)
-- (from STRING)
require -- from STRING
represents_a_double: string_is_double

to_integer: INTEGER
-- Integer value;
-- for example, when applied to "123", will yield 123
-- (from STRING)
require -- from STRING
is_integer: string_is_integer

to_lower
-- Convert to lower case.
-- (from STRING)

to_real: REAL
-- Real value;
-- for example, when applied to "123.0", will yield 123.0
-- (from STRING)
require -- from STRING
represents_a_real: string_is_real

to_upper
-- Convert to upper case.
-- (from STRING)

feature -- Duplication

multiply (n: INTEGER)
-- Duplicate a string within itself
-- ("hello").multiply(3) => "hellohellohello"
-- (from STRING)
require -- from STRING
meaningful_multiplier: n >= 1

substring (n1, n2: INTEGER): like Current
-- Copy of substring containing all characters at indices
-- between n1 and n2
-- (from STRING)
ensure -- from STRING
new_result_count: Result.count = n2 - n1 + 1 or Result.count = 0

feature -- Basic operations

abs (n: INTEGER): INTEGER
-- Absolute value of n
-- (from BASIC_ROUTINES)
ensure -- from BASIC_ROUTINES
non_negative_result: Result >= 0

append_substring (s: STRING; n1, n2: INTEGER)
-- Append substring `s.substring (n1, n2)' to Current.
-- Faster than append s.substring (n1, n2).
require
string_exists: s /= void
meaningful_origin: 1 <= n1
meaningful_interval: n1 <= n2
meaningful_end: n2 <= s.count

bottom_int_div (n1, n2: INTEGER): INTEGER
-- Greatest lower bound of the integer division of n1 by n2
-- (from BASIC_ROUTINES)

deep_traversal (object: ANY)
-- Perform a deep recursive traversal on
-- the transitive closure of the object network
-- reachable from root object.
-- (from EXT_INTERNAL)
require -- from EXT_INTERNAL
root_object_non_void: object /= void

field_clean (i: INTEGER; object: ANY): BOOLEAN
-- Clean i-th field of object.
-- (from EXT_INTERNAL)
require -- from EXT_INTERNAL
object_exists: object /= void

field_copy (i: INTEGER; object, value: ANY): BOOLEAN
-- Copy value in i-th field of object.
-- (from EXT_INTERNAL)
require -- from EXT_INTERNAL
object_exists: object /= void
value_exists: value /= void

get_complex_value (obj: ANY; str: STRING)
-- Retrieve string value of reference object obj and put in str.
require
object_exists: obj /= void
str_exists: str /= void

get_value (obj: ANY; str: STRING)
-- Retrieve string value of obj and put in str.
require
str_exists: str /= void

is_marked (obj: ANY): BOOLEAN
-- Is obj marked?
-- (from EXT_INTERNAL)
require -- from EXT_INTERNAL
object_exists: obj /= void

mark (obj: ANY)
-- Mark object obj
-- (from EXT_INTERNAL)
require -- from EXT_INTERNAL
object_exists: obj /= void

nb_classes: INTEGER
-- Number of dynamic types in current system
-- (from EXT_INTERNAL)

object_finish_action (object: ANY)
-- Do nothing.
-- (To be redefined in heir.)
-- (from EXT_INTERNAL)

object_init_action (object: ANY)
-- Do nothing.
-- (To be redefined in heir.)
-- (from EXT_INTERNAL)

parse (s: STRING): STRING
-- Parse string s by replacing each pattern ":<name>"
-- with the Eiffel object description whose name
-- also matches "<name>".

reference_object_action (i: INTEGER; object: ANY)
-- Do nothing.
-- (To be redefined in heir.)
-- (from EXT_INTERNAL)

replace
-- Replace all occurences of :key by `ht.item (":key")'

rsign (r: REAL): INTEGER
-- Sign of r:
-- -1 if r < 0
-- 0 if r = 0
-- +1 if r > 0
-- (from BASIC_ROUTINES)
ensure -- from BASIC_ROUTINES
correct_negative: (r < 0) = (Result = - 1)
correct_zero: (r = 0) = (Result = 0)
correct_positive: (r > 0) = (Result = + 1)

sign (n: INTEGER): INTEGER
-- Sign of n:
-- -1 if n < 0
-- 0 if n = 0
-- +1 if n > 0
-- (from BASIC_ROUTINES)
ensure -- from BASIC_ROUTINES
correct_negative: (n < 0) = (Result = - 1)
correct_zero: (n = 0) = (Result = 0)
correct_positive: (n > 0) = (Result = + 1)

simple_object_action (type, i: INTEGER; object: ANY)
-- Do nothing.
-- (To be redefined in heir.)
-- (from EXT_INTERNAL)

store_action (object: ANY)
-- Do nothing.
-- (To be redefined in heir.)
-- (from EXT_INTERNAL)

switch_mark (obj: ANY)
-- Unmark obj if marked or mark it if unmarked.
-- (from EXT_INTERNAL)
require -- from EXT_INTERNAL
object_exists: obj /= void

traversal (object: ANY)
-- Traverse the entire object structure starting with root obj.
-- An object in the Eiffel run-time system includes the following:
--    a) Reference objects instance of a class type
--    b) Special reference objects allocated to refer to a
--              variable size object like STRING and ARRAY
--    c) Reference objects created for a generic type instantiated
--                      as an expanded type or BITS n
-- LIMITATION: Current version excludes objects in the Eiffel
-- run-time system where expanded objects are encapsulated within
-- other objects
-- (from EXT_INTERNAL)
require -- from EXT_INTERNAL
object_exists: object /= void

unmark (obj: ANY)
-- Unmark object obj
-- (from EXT_INTERNAL)
require -- from EXT_INTERNAL
object_exists: obj /= void

unmark_structure (obj: ANY)
-- Unmark structure of objects.
-- (from EXT_INTERNAL)
require -- from EXT_INTERNAL
object_exists: obj /= void

up_int_div (n1, n2: INTEGER): INTEGER
-- Least upper bound of the integer division
-- of n1 by n2
-- (from BASIC_ROUTINES)

feature -- Conformance

is_instance_of (object: ANY; type_id: INTEGER): BOOLEAN
-- Is object an instance of type type_id?
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void

type_conforms_to (type1, type2: INTEGER): BOOLEAN
-- Does type1 conform to type2?
-- (from INTERNAL)

feature -- Creation

dynamic_type_from_string (class_type: STRING): INTEGER
-- Dynamic type corresponding to class_type.
-- If no dynamic type available, returns -1.
-- (from INTERNAL)
require -- from INTERNAL
class_type_not_void: class_type /= void
ensure -- from INTERNAL
valid_result: Result = - 1 or else Result >= 0

new_instance_of (type_id: INTEGER): ANY
-- New instance of dynamic type_id.
-- Note: returned object is not initialized and may
-- hence violate its invariant.
-- (from INTERNAL)

feature -- Output

out: like Current
-- Printable representation
-- (from STRING)

feature -- Version

compiler_version: INTEGER
-- (from INTERNAL)

invariant

-- from ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
-- from STRING
extendible: extendible
compare_character: not object_comparison
index_set_has_same_count: index_set.count = count
-- from INDEXABLE
index_set_not_void: index_set /= void
-- from RESIZABLE
increase_by_at_least_one: minimal_increase >= 1
-- from BOUNDED
valid_count: count <= capacity
full_definition: full = (count = capacity)
-- from FINITE
empty_definition: is_empty = (count = 0)
non_negative_count: count >= 0
-- from COMPARABLE
irreflexive_comparison: not (Current < Current)

end -- class SQL_SCAN