indexing
description: "Common ancestors to all STRING classes."
date: "$Date: 2006-09-20 15:19:17 -0700 (Wed, 20 Sep 2006) $"
revision: "$Revision: 63744 $"
deferred class interface
STRING_GENERAL
convert
as_string_32: {STRING_32},
to_cil: {SYSTEM_STRING}
feature
code (i: INTEGER_32): NATURAL_32
`i'
require
valid_index: valid_index (i)
generating_type: STRING_8
ANY
generator: STRING_8
ANY
hash_code: INTEGER_32
HASHABLE
ensure HASHABLE
good_hash_value: Result >= 0
index_of_code (c: like code; start_index: INTEGER_32): INTEGER_32
`c'`start_index'
require
start_large_enough: start_index >= 1
start_small_enough: start_index <= count + 1
ensure
valid_result: Result = 0 or (start_index <= Result and Result <= count)
zero_if_absent: (Result = 0) = not substring (start_index, count).has_code (c)
found_if_present: substring (start_index, count).has_code (c) implies code (Result) = c
none_before: substring (start_index, count).has_code (c) implies not substring (start_index, Result - 1).has_code (c)
feature
frozen deep_equal (some: ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
shallow_implies_deep: standard_equal (some, other) implies Result
both_or_none_void: (some = Void) implies (Result = (other = Void))
same_type: (Result and (some /= Void)) implies some.same_type (other)
symmetric: Result implies deep_equal (other, some)
frozen equal (some: ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.is_equal (other))
is_equal (other: like Current): BOOLEAN
`other'
COMPARABLE
require ANY
other_not_void: other /= Void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
ensure then COMPARABLE
trichotomy: Result = (not (Current < other) and not (other < Current))
max (other: like Current): like Current
`other'
COMPARABLE
require COMPARABLE
other_exists: other /= Void
ensure COMPARABLE
current_if_not_smaller: Current >= other implies Result = Current
other_if_smaller: Current < other implies Result = other
min (other: like Current): like Current
`other'
COMPARABLE
require COMPARABLE
other_exists: other /= Void
ensure COMPARABLE
current_if_not_greater: Current <= other implies Result = Current
other_if_greater: Current > other implies Result = other
frozen standard_equal (some: ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.standard_is_equal (other))
frozen standard_is_equal (other: like Current): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
same_type: Result implies same_type (other)
symmetric: Result implies other.standard_is_equal (Current)
three_way_comparison (other: like Current): INTEGER_32
`other'
COMPARABLE
require COMPARABLE
other_exists: other /= Void
ensure 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
`other'
COMPARABLE
require PART_COMPARABLE
other_exists: other /= Void
ensure then COMPARABLE
asymmetric: Result implies not (other < Current)
infix "<=" (other: like Current): BOOLEAN
`other'
COMPARABLE
require PART_COMPARABLE
other_exists: other /= Void
ensure then COMPARABLE
definition: Result = ((Current < other) or is_equal (other))
infix ">" (other: like Current): BOOLEAN
`other'
COMPARABLE
require PART_COMPARABLE
other_exists: other /= Void
ensure then COMPARABLE
definition: Result = (other < Current)
infix ">=" (other: like Current): BOOLEAN
`other'
COMPARABLE
require PART_COMPARABLE
other_exists: other /= Void
ensure then COMPARABLE
definition: Result = (other <= Current)
feature
capacity: INTEGER_32
ensure
capacity_non_negative: Result >= 0
conforms_to (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
count: INTEGER_32
ensure
count_non_negative: Result >= 0
has_code (c: like code): BOOLEAN
`c'
ensure then
false_if_empty: count = 0 implies not Result
true_if_first: count > 0 and then code (1) = c implies Result
recurse: (count > 0 and then code (1) /= c) implies (Result = substring (2, count).has_code (c))
is_empty: BOOLEAN
is_hashable: BOOLEAN
HASHABLE
ensure HASHABLE
ok_if_not_default: Result implies (Current /= default)
is_string_32: BOOLEAN
`Current'
is_string_8: BOOLEAN
`Current'
is_valid_as_string_8: BOOLEAN
`Current'
same_type (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
definition: Result = (conforms_to (other) and other.conforms_to (Current))
valid_code (v: like code): BOOLEAN
`v'
valid_index (i: INTEGER_32): BOOLEAN
`i'
feature
append (s: STRING_GENERAL)
`s'
require
argument_not_void: s /= Void
compatible_strings: is_string_8 implies s.is_valid_as_string_8
ensure
new_count: count = old count + old s.count
appended: elks_checking implies to_string_32.is_equal (old to_string_32.twin + old s.to_string_32.twin)
append_code (c: like code)
`c'
require
valid_code: valid_code (c)
ensure then
item_inserted: code (count) = c
new_count: count = old count + 1
stable_before: elks_checking implies substring (1, count - 1).is_equal (old twin)
feature
remove (i: INTEGER_32)
`i'
require
valid_index: valid_index (i)
ensure
new_count: count = old count - 1
removed: elks_checking implies to_string_32.is_equal (old substring (1, i - 1).to_string_32 + old substring (i + 1, count).to_string_32)
feature
resize (newsize: INTEGER_32)
`newsize'
require
new_size_non_negative: newsize >= 0
feature
as_string_32: STRING_32
`Current'
STRING_GENERALto_string_32
ensure
as_string_32_not_void: Result /= Void
identity: (is_string_32 and Result = Current) or (not is_string_32 and Result /= Current)
as_string_8: STRING_8
`Current'`Current'
ensure
as_string_8_not_void: Result /= Void
identity: (is_string_8 and Result = Current) or (not is_string_8 and Result /= Current)
frozen to_cil: SYSTEM_STRING
`1'count
require
is_dotnet: {PLATFORM}.is_dotnet
ensure
to_cil_not_void: Result /= Void
to_string_32: STRING_32
`Current'
STRING_GENERALas_string_32
ensure
as_string_32_not_void: Result /= Void
identity: (is_string_32 and Result = Current) or (not is_string_32 and Result /= Current)
to_string_8: STRING_8
`Current'
require
is_valid_as_string_8: is_valid_as_string_8
ensure
as_string_8_not_void: Result /= Void
identity: (is_string_8 and Result = Current) or (not is_string_8 and Result /= Current)
feature
copy (other: like Current)
`other'
ANY
require ANY
other_not_void: other /= Void
type_identity: same_type (other)
ensure ANY
is_equal: is_equal (other)
frozen deep_copy (other: like Current)
copy`other'deep_twin
ANY
require ANY
other_not_void: other /= Void
ensure ANY
deep_equal: deep_equal (Current, other)
frozen deep_twin: like Current
ANY
ensure ANY
deep_equal: deep_equal (Current, Result)
frozen standard_copy (other: like Current)
`other'
ANY
require ANY
other_not_void: other /= Void
type_identity: same_type (other)
ensure ANY
is_standard_equal: standard_is_equal (other)
frozen standard_twin: like Current
`other'
ANY
ensure ANY
standard_twin_not_void: Result /= Void
equal: standard_equal (Result, Current)
substring (start_index, end_index: INTEGER_32): like Current
`start_index'`end_index'
ensure
substring_not_void: Result /= Void
substring_count: Result.count = end_index - start_index + 1 or Result.count = 0
first_item: Result.count > 0 implies Result.code (1) = code (start_index)
recurse: Result.count > 0 implies Result.substring (2, Result.count).is_equal (substring (start_index + 1, end_index))
frozen twin: like Current
`Current'
twincopycopy
ANY
ensure ANY
twin_not_void: Result /= Void
is_equal: Result.is_equal (Current)
feature
frozen default: like Current
ANY
frozen default_pointer: POINTER
`POINTER'
`p'default
`p'`POINTER'
ANY
default_rescue
ANY
frozen do_nothing
ANY
feature
io: STD_FILES
ANY
out: STRING_8
ANYtagged_out
ANY
print (some: ANY)
`some'
ANY
frozen tagged_out: STRING_8
ANYout
ANY
feature
operating_environment: OPERATING_ENVIRONMENT
ANY
feature
put_code (v: like code; i: INTEGER_32)
`v'`i'
require
valid_code: valid_code (v)
valid_index: valid_index (i)
ensure
inserted: code (i) = v
stable_count: count = old count
stable_before_i: elks_checking implies substring (1, i - 1).is_equal (old substring (1, i - 1))
stable_after_i: elks_checking implies substring (i + 1, count).is_equal (old substring (i + 1, count))
invariant
COMPARABLE
irreflexive_comparison: not (Current < Current)
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end STRING_GENERAL