indexing
description: "Implementation of DB_STORE"
legal: "See notice at end of class."
status: "See notice at end of class."
date: "$Date: 2006-01-22 18:25:44 -0800 (Sun, 22 Jan 2006) $"
revision: "$Revision: 56675 $"
class interface
DATABASE_STORE [reference G -> DATABASE create default_create end]
create
make (size: INTEGER_32)
create {DATABASE_STORE}
string_make (n: INTEGER_32)
`n'
STRING_8
require STRING_8
non_negative_size: n >= 0
ensure STRING_8
empty_string: count = 0
area_allocated: capacity >= n
scan_make (i: INTEGER_32)
SQL_SCAN
feature
adapt (s: STRING_8): like Current
`s'
`s'
STRING_8
ensure STRING_8
adapt_not_void: Result /= Void
shared_implementation: Result.shared_with (s)
from_c (c_string: POINTER)
`c_string'
STRING_8
require STRING_8
c_string_exists: c_string /= default_pointer
ensure STRING_8
no_zero_byte: not has ('%U')
from_c_substring (c_string: POINTER; start_pos, end_pos: INTEGER_32)
`c_string'
STRING_8
require STRING_8
c_string_exists: c_string /= default_pointer
start_position_big_enough: start_pos >= 1
end_position_big_enough: start_pos <= end_pos + 1
ensure STRING_8
valid_count: count = end_pos - start_pos + 1
make (size: INTEGER_32)
scan_make (i: INTEGER_32)
SQL_SCAN
string_make (n: INTEGER_32)
`n'
STRING_8
require STRING_8
non_negative_size: n >= 0
ensure STRING_8
empty_string: count = 0
area_allocated: capacity >= n
format_make
DB_FORMAT
make_empty
STRING_8
ensure STRING_8
empty: count = 0
area_allocated: capacity >= 0
make_filled (c: CHARACTER_8; n: INTEGER_32)
`n'`c'
STRING_8
require STRING_8
valid_count: n >= 0
ensure STRING_8
count_set: count = n
area_allocated: capacity >= n
filled: occurrences (c) = count
make_from_c (c_string: POINTER)
`c_string'
STRING_8
require STRING_8
c_string_exists: c_string /= default_pointer
make_from_cil (a_system_string: SYSTEM_STRING)
`a_system_string'
STRING_8
require STRING_8
is_dotnet: {PLATFORM}.is_dotnet
make_from_string (s: STRING_8)
`s'
STRING_8
require STRING_8
string_exists: s /= Void
ensure STRING_8
not_shared_implementation: Current /= s implies not shared_with (s)
initialized: same_string (s)
feature
area: SPECIAL [CHARACTER_8]
TO_SPECIAL
bit_type: INTEGER_32 is 8
INTERNAL
boolean_field (i: INTEGER_32; object: ANY): BOOLEAN
`i'`object'
INTERNAL
require 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_32 is 3
INTERNAL
character_32_type: INTEGER_32 is 12
INTERNALWide_character_type
INTERNAL
character_8_type: INTEGER_32 is 2
INTERNALCharacter_type
INTERNAL
character_field (i: INTEGER_32; object: ANY): CHARACTER_8
`i'`object'
INTERNAL
require 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_32 is 2
INTERNALCharacter_8_type
INTERNAL
class_name (object: ANY): STRING_8
`object'
INTERNAL
require INTERNAL
object_not_void: object /= Void
class_name_of_type (type_id: INTEGER_32): STRING_8
`type_id'
INTERNAL
require INTERNAL
type_id_nonnegative: type_id >= 0
code (i: INTEGER_32): NATURAL_32
`i'
STRING_8
require STRING_GENERAL
valid_index: valid_index (i)
db_spec: DATABASE
HANDLE_SPEC
ensure HANDLE_SPEC
not_void: Result /= Void
double_field (i: INTEGER_32; object: ANY): REAL_64
`i'`object'
INTERNALreal_64_field
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
real_64_field: field_type (i, object) = real_64_type
double_type: INTEGER_32 is 6
INTERNALReal_64_type
INTERNAL
dynamic_type (object: ANY): INTEGER_32
`object'
INTERNAL
require INTERNAL
object_not_void: object /= Void
ensure INTERNAL
dynamic_type_nonnegative: Result >= 0
expanded_field_type (i: INTEGER_32; object: ANY): STRING_8
`i'
`object'
INTERNAL
require 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 INTERNAL
result_exists: Result /= Void
expanded_type: INTEGER_32 is 7
INTERNAL
false_constant: STRING_8 is "false"
STRING_8
field (i: INTEGER_32; object: ANY): ANY
`i'`object'
INTERNAL
require 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_32; object: ANY): STRING_8
`i'`object'
INTERNAL
require 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 INTERNAL
result_exists: Result /= Void
field_name_of_type (i: INTEGER_32; type_id: INTEGER_32): STRING_8
`i'`type_id'
INTERNAL
require INTERNAL
type_id_nonnegative: type_id >= 0
index_large_enough: i >= 1
index_small_enought: i <= field_count_of_type (type_id)
field_offset (i: INTEGER_32; object: ANY): INTEGER_32
`i'`object'
INTERNAL
require 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_static_type_of_type (i: INTEGER_32; type_id: INTEGER_32): INTEGER_32
`i'`type_id'
INTERNAL
require INTERNAL
type_id_nonnegative: type_id >= 0
index_large_enough: i >= 1
index_small_enough: i <= field_count_of_type (type_id)
ensure INTERNAL
field_type_nonnegative: Result >= 0
field_type (i: INTEGER_32; object: ANY): INTEGER_32
`i'`object'
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
ensure INTERNAL
field_type_nonnegative: Result >= 0
field_type_of_type (i: INTEGER_32; type_id: INTEGER_32): INTEGER_32
`i'`type_id'
INTERNAL
require INTERNAL
type_id_nonnegative: type_id >= 0
index_large_enough: i >= 1
index_small_enough: i <= field_count_of_type (type_id)
ensure INTERNAL
field_type_nonnegative: Result >= 0
fuzzy_index (other: STRING_8; start: INTEGER_32; fuzz: INTEGER_32): INTEGER_32
`other'start
`fuzz'`other'
STRING_8
require STRING_8
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
generating_type: STRING_8
ANY
generator: STRING_8
ANY
generic_count (obj: ANY): INTEGER_32
`obj'
INTERNAL
require INTERNAL
obj_not_void: obj /= Void
generic_count_of_type (type_id: INTEGER_32): INTEGER_32
`type_id'
INTERNAL
require INTERNAL
type_id_nonnegative: type_id >= 0
generic_dynamic_type (object: ANY; i: INTEGER_32): INTEGER_32
`object'
`i'
INTERNAL
require INTERNAL
object_not_void: object /= Void
object_generic: generic_count (object) > 0
i_valid: i > 0 and i <= generic_count (object)
ensure INTERNAL
dynamic_type_nonnegative: Result >= 0
generic_dynamic_type_of_type (type_id: INTEGER_32; i: INTEGER_32): INTEGER_32
`type_id'`i'
INTERNAL
require INTERNAL
type_id_nonnegative: type_id >= 0
type_id_generic: generic_count_of_type (type_id) > 0
i_valid: i > 0 and i <= generic_count_of_type (type_id)
ensure INTERNAL
dynamic_type_nonnegative: Result >= 0
hash_code: INTEGER_32
STRING_8
ensure HASHABLE
good_hash_value: Result >= 0
index_of (c: CHARACTER_8; start_index: INTEGER_32): INTEGER_32
`c'`start_index'
STRING_8
require STRING_8
start_large_enough: start_index >= 1
start_small_enough: start_index <= count + 1
ensure STRING_8
valid_result: Result = 0 or (start_index <= Result and Result <= count)
zero_if_absent: (Result = 0) = not substring (start_index, count).has (c)
found_if_present: substring (start_index, count).has (c) implies item (Result) = c
none_before: substring (start_index, count).has (c) implies not substring (start_index, Result - 1).has (c)
index_of_code (c: like code; start_index: INTEGER_32): INTEGER_32
`c'`start_index'
STRING_GENERAL
require STRING_GENERAL
start_large_enough: start_index >= 1
start_small_enough: start_index <= count + 1
ensure STRING_GENERAL
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)
integer_16_field (i: INTEGER_32; object: ANY): INTEGER_16
`i'`object'
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
integer_16_field: field_type (i, object) = integer_16_type
integer_16_type: INTEGER_32 is 10
INTERNAL
integer_32_field (i: INTEGER_32; object: ANY): INTEGER_32
`i'`object'
INTERNALinteger_field
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
integer_32_field: field_type (i, object) = integer_32_type
integer_32_type: INTEGER_32 is 4
INTERNALInteger_type
INTERNAL
integer_64_field (i: INTEGER_32; object: ANY): INTEGER_64
`i'`object'
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
integer_64_field: field_type (i, object) = integer_64_type
integer_64_type: INTEGER_32 is 11
INTERNAL
integer_8_field (i: INTEGER_32; object: ANY): INTEGER_8
`i'`object'
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
integer_8_field: field_type (i, object) = integer_8_type
integer_8_type: INTEGER_32 is 9
INTERNAL
integer_field (i: INTEGER_32; object: ANY): INTEGER_32
`i'`object'
INTERNALinteger_32_field
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
integer_32_field: field_type (i, object) = integer_32_type
integer_type: INTEGER_32 is 4
INTERNALInteger_32_type
INTERNAL
item (i: INTEGER_32): CHARACTER_8 assign put
`i'
STRING_8infix "@"
STRING_8
require TABLE
valid_key: valid_index (i)
require TO_SPECIAL
valid_index: valid_index (i)
item_code (i: INTEGER_32): INTEGER_32
`i'
STRING_8
require STRING_8
index_small_enough: i <= count
index_large_enough: i > 0
last_index_of (c: CHARACTER_8; start_index_from_end: INTEGER_32): INTEGER_32
`c'
STRING_8
require STRING_8
start_index_small_enough: start_index_from_end <= count
start_index_large_enough: start_index_from_end >= 1
ensure STRING_8
last_index_of_non_negative: Result >= 0
correct_place: Result > 0 implies item (Result) = c
max_predefined_type: INTEGER_32 is 16
INTERNAL
natural_16_field (i: INTEGER_32; object: ANY): NATURAL_16
`i'`object'
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
natural_16_field: field_type (i, object) = natural_16_type
natural_16_type: INTEGER_32 is 14
INTERNAL
natural_32_field (i: INTEGER_32; object: ANY): NATURAL_32
`i'`object'
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
natural_32_field: field_type (i, object) = natural_32_type
natural_32_type: INTEGER_32 is 15
INTERNAL
natural_64_field (i: INTEGER_32; object: ANY): NATURAL_64
`i'`object'
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
natural_64_field: field_type (i, object) = natural_64_type
natural_64_type: INTEGER_32 is 16
INTERNAL
natural_8_field (i: INTEGER_32; object: ANY): NATURAL_8
`i'`object'
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
natural_8_field: field_type (i, object) = natural_8_type
natural_8_type: INTEGER_32 is 13
INTERNAL
none_type: INTEGER_32 is -2
INTERNAL
pointer_field (i: INTEGER_32; object: ANY): POINTER
`i'`object'
INTERNAL
require 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_32 is 0
INTERNAL
real_32_field (i: INTEGER_32; object: ANY): REAL_32
`i'`object'
INTERNALreal_field
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
real_32_field: field_type (i, object) = real_32_type
real_32_type: INTEGER_32 is 5
INTERNALReal_type
INTERNAL
real_64_field (i: INTEGER_32; object: ANY): REAL_64
`i'`object'
INTERNALdouble_field
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
real_64_field: field_type (i, object) = real_64_type
real_64_type: INTEGER_32 is 6
INTERNALDouble_type
INTERNAL
real_field (i: INTEGER_32; object: ANY): REAL_32
`i'`object'
INTERNALreal_32_field
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
real_32_field: field_type (i, object) = real_32_type
real_type: INTEGER_32 is 5
INTERNALReal_32_type
INTERNAL
reference_type: INTEGER_32 is 1
INTERNAL
shared_with (other: STRING_8): BOOLEAN
`other'
STRING_8
string: STRING_8
`Current'
STRING_8
ensure STRING_8
string_not_void: Result /= Void
string_type: Result.same_type ("")
first_item: count > 0 implies Result.item (1) = item (1)
recurse: count > 1 implies Result.substring (2, count).is_equal (substring (2, count).string)
substring_index (other: STRING_8; start_index: INTEGER_32): INTEGER_32
STRING_8
require STRING_8
other_not_void: other /= Void
valid_start_index: start_index >= 1 and start_index <= count + 1
ensure STRING_8
valid_result: Result = 0 or else (start_index <= Result and Result <= count - other.count + 1)
zero_if_absent: (Result = 0) = not substring (start_index, count).has_substring (other)
at_this_index: Result >= start_index implies other.same_string (substring (Result, Result + other.count - 1))
none_before: Result > start_index implies not substring (start_index, Result + other.count - 2).has_substring (other)
substring_index_in_bounds (other: STRING_8; start_pos, end_pos: INTEGER_32): INTEGER_32
`other'`start_pos'
`end_pos'
STRING_8
require STRING_8
other_nonvoid: other /= Void
other_notempty: not other.is_empty
start_pos_large_enough: start_pos >= 1
start_pos_small_enough: start_pos <= count
end_pos_large_enough: end_pos >= start_pos
end_pos_small_enough: end_pos <= count
ensure STRING_8
correct_place: Result > 0 implies other.is_equal (substring (Result, Result + other.count - 1))
true_constant: STRING_8 is "true"
STRING_8
type_name (object: ANY): STRING_8
`object'`object'
INTERNAL
require INTERNAL
object_not_void: object /= Void
type_name_of_type (type_id: INTEGER_32): STRING_8
`type_id'`type_id'
INTERNAL
require INTERNAL
type_id_nonnegative: type_id >= 0
wide_character_type: INTEGER_32 is 12
INTERNALCharacter_32_type
INTERNAL
infix "@" (i: INTEGER_32): CHARACTER_8 assign put
`i'
STRING_8item
STRING_8
require TABLE
valid_key: valid_index (i)
require TO_SPECIAL
valid_index: valid_index (i)
feature
additional_space: INTEGER_32
RESIZABLE
ensure RESIZABLE
at_least_one: Result >= 1
bit_size (i: INTEGER_32; object: ANY): INTEGER_32
`i'`object'
INTERNAL
require 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 INTERNAL
positive_result: Result > 0
capacity: INTEGER_32
STRING_8
require BOUNDED
True
require STRING_GENERAL
True
ensure STRING_GENERAL
capacity_non_negative: Result >= 0
count: INTEGER_32
STRING_8
field_count (object: ANY): INTEGER_32
`object'
INTERNAL
require INTERNAL
object_not_void: object /= Void
field_count_of_type (type_id: INTEGER_32): INTEGER_32
`type_id'
INTERNAL
require INTERNAL
type_id_nonnegative: type_id >= 0
growth_percentage: INTEGER_32 is 50
RESIZABLE
index_set: INTEGER_INTERVAL
STRING_8
require INDEXABLE
True
ensure INDEXABLE
not_void: Result /= Void
ensure then STRING_8
Result.count = count
minimal_increase: INTEGER_32 is 5
RESIZABLE
occurrences (c: CHARACTER_8): INTEGER_32
`c'
STRING_8
require BAG
True
ensure BAG
non_negative_occurrences: Result >= 0
ensure then STRING_8
zero_if_empty: count = 0 implies Result = 0
recurse_if_not_found_at_first_position: (count > 0 and then item (1) /= c) implies Result = substring (2, count).occurrences (c)
recurse_if_found_at_first_position: (count > 0 and then item (1) = c) implies Result = 1 + substring (2, count).occurrences (c)
physical_size (object: ANY): INTEGER_32
`object'
INTERNAL
require INTERNAL
object_not_void: object /= Void
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_case_insensitive_equal (other: like Current): BOOLEAN
`other'
STRING_8
require STRING_8
other_not_void: other /= Void
ensure STRING_8
symmetric: Result implies other.is_case_insensitive_equal (Current)
consistent: standard_is_equal (other) implies Result
valid_result: as_lower.is_equal (other.as_lower) implies Result
is_equal (other: like Current): BOOLEAN
`other'
STRING_8
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
same_string (other: STRING_8): BOOLEAN
`Current'`other'
STRING_8
require STRING_8
other_not_void: other /= Void
ensure STRING_8
definition: Result = string.is_equal (other.string)
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'
STRING_8
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
changeable_comparison_criterion: BOOLEAN is False
STRING_8
conforms_to (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
extendible: BOOLEAN is True
STRING_8
full: BOOLEAN
BOUNDED
has (c: CHARACTER_8): BOOLEAN
`c'
STRING_8
require CONTAINER
True
ensure CONTAINER
not_found_in_empty: Result implies not is_empty
ensure then STRING_8
false_if_empty: count = 0 implies not Result
true_if_first: count > 0 and then item (1) = c implies Result
recurse: (count > 0 and then item (1) /= c) implies (Result = substring (2, count).has (c))
has_code (c: like code): BOOLEAN
`c'
STRING_GENERAL
ensure then STRING_GENERAL
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))
has_substring (other: STRING_8): BOOLEAN
`Current'`other'
STRING_8
require STRING_8
other_not_void: other /= Void
ensure STRING_8
false_if_too_small: count < other.count implies not Result
true_if_initial: (count >= other.count and then other.same_string (substring (1, other.count))) implies Result
recurse: (count >= other.count and then not other.same_string (substring (1, other.count))) implies (Result = substring (2, count).has_substring (other))
ht: HASH_TABLE [ANY, STRING_8]
STRING_HDL
ht_order: ARRAYED_LIST [STRING_8]
ht
STRING_HDL
immediate_execution: BOOLEAN
`no'
DB_EXEC_USE
string_is_boolean: BOOLEAN
`Current'
STRING_8
ensure STRING_8
is_boolean: Result = (true_constant.same_string (as_lower) or false_constant.same_string (as_lower))
string_is_double: BOOLEAN
`Current'
STRING_8
is_empty: BOOLEAN
FINITE
require CONTAINER
True
require STRING_GENERAL
True
is_hashable: BOOLEAN
HASHABLE
ensure HASHABLE
ok_if_not_default: Result implies (Current /= default)
is_inserted (v: CHARACTER_8): BOOLEAN
`v'
`has (v)'
COLLECTION
string_is_integer: BOOLEAN
`Current'
STRING_8is_integer_32
STRING_8
is_integer_16: BOOLEAN
`Current'
STRING_8
is_integer_32: BOOLEAN
`Current'
STRING_8is_integer
STRING_8
is_integer_64: BOOLEAN
`Current'
STRING_8
is_integer_8: BOOLEAN
`Current'
STRING_8
is_mapped (key: STRING_8): BOOLEAN
`key'
STRING_HDL
require STRING_HDL
ht_not_void: ht /= Void
keys_exists: key /= Void
is_marked (obj: ANY): BOOLEAN
`obj'
INTERNAL
require INTERNAL
object_exists: obj /= Void
is_natural: BOOLEAN
`Current'
STRING_8is_natural_32
STRING_8
is_natural_16: BOOLEAN
`Current'
STRING_8
is_natural_32: BOOLEAN
`Current'
STRING_8is_natural
STRING_8
is_natural_64: BOOLEAN
`Current'
STRING_8
is_natural_8: BOOLEAN
`Current'
STRING_8
is_number_sequence: BOOLEAN
`Current'
STRING_8
is_pre_ecma_mapping_disabled: BOOLEAN
INTERNAL_HELPER
string_is_real: BOOLEAN
`Current'
STRING_8
is_special (object: ANY): BOOLEAN
`object'
INTERNAL
require INTERNAL
object_not_void: object /= Void
is_special_any_type (type_id: INTEGER_32): BOOLEAN
`type_id'
INTERNAL
require INTERNAL
type_id_nonnegative: type_id >= 0
is_special_type (type_id: INTEGER_32): BOOLEAN
`type_id'
INTERNAL
require INTERNAL
type_id_nonnegative: type_id >= 0
is_string_32: BOOLEAN is False
STRING_8
is_string_8: BOOLEAN is True
STRING_8
is_tracing: BOOLEAN
DB_EXEC_USE
is_tuple (object: ANY): BOOLEAN
`object'
INTERNAL
require INTERNAL
object_not_void: object /= Void
is_tuple_type (type_id: INTEGER_32): BOOLEAN
`type_id'
INTERNAL
require INTERNAL
type_id_nonnegative: type_id >= 0
is_valid_as_string_8: BOOLEAN is True
`Current'
STRING_8
is_valid_type_string (s: STRING_8): BOOLEAN
`s'
INTERNAL_HELPER
require INTERNAL_HELPER
s_not_void: s /= Void
s_not_empty: not s.is_empty
mapped_type (a_type: STRING_8): STRING_8
is_pre_ecma_mapping_disabled`a_type'
INTERNAL_HELPER
require INTERNAL_HELPER
a_type_not_void: a_type /= Void
ensure INTERNAL_HELPER
mapped_type_not_void: Result /= Void
mapped_value (key: STRING_8): ANY
`key'
STRING_HDL
require STRING_HDL
ht_not_void: ht /= Void
key_exists: key /= Void
key_mapped: is_mapped (key)
ensure STRING_HDL
result_exists: Result /= Void
object_comparison: BOOLEAN
equal`='
`='
CONTAINER
owns_repository: BOOLEAN
ensure
existence_condition: Result = (repository /= Void)
prunable: BOOLEAN
STRING_8
repository: DATABASE_REPOSITORY [G]
resizable: BOOLEAN
capacity
RESIZABLE
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))
trace_output: FILE
DB_EXEC_USE
valid_code (v: NATURAL_32): BOOLEAN
`v'
STRING_8
valid_index (i: INTEGER_32): BOOLEAN
`i'
STRING_8
require TABLE
True
require STRING_GENERAL
True
require TO_SPECIAL
True
ensure then INDEXABLE
only_if_in_index_set: Result implies ((i >= index_set.lower) and (i <= index_set.upper))
feature
clear_all
STRING_HDL
require STRING_8
True
require STRING_HDL
ht_not_void: ht /= Void
ensure STRING_8
is_empty: count = 0
same_capacity: capacity = old capacity
compare_objects
equal
`='
CONTAINER
require CONTAINER
changeable_comparison_criterion: changeable_comparison_criterion
ensure CONTAINER
object_comparison
compare_references
`='
equal
CONTAINER
require CONTAINER
changeable_comparison_criterion: changeable_comparison_criterion
ensure CONTAINER
reference_comparison: not object_comparison
disable_pre_ecma_mapping
is_pre_ecma_mapping_disabled
INTERNAL_HELPER
ensure INTERNAL_HELPER
is_pre_ecma_mapping_disabled_set: is_pre_ecma_mapping_disabled
enable_pre_ecma_mapping
is_pre_ecma_mapping_disabled
INTERNAL_HELPER
ensure INTERNAL_HELPER
is_pre_ecma_mapping_disabled_set: not is_pre_ecma_mapping_disabled
set_immediate
`EXECUTE IMMEDIATE'
DB_EXEC_USE
ensure DB_EXEC_USE
execution_status: immediate_execution
set_map_name (n: ANY; key: STRING_8)
`n'`key'
`n'`Void'
STRING_HDL
require STRING_HDL
ht_not_void: ht /= Void
key_exists: key /= Void
not_key_in_table: not is_mapped (key)
ensure STRING_HDL
ht.count = old ht.count + 1
set_repository (one_repository: DATABASE_REPOSITORY [G])
`one_repository'
require
parameter_not_void: one_repository /= Void
ensure then
repository_not_void: repository /= Void
set_trace
DB_EXEC_USE
ensure DB_EXEC_USE
trace_status: is_tracing
unset_immediate
`PREPARE'`EXECUTE'
DB_EXEC_USE
ensure DB_EXEC_USE
execution_status: not immediate_execution
unset_map_name (key: STRING_8)
`key'
STRING_HDL
require STRING_HDL
ht_not_void: ht /= Void
key_exists: key /= Void
item_exists: is_mapped (key)
ensure STRING_HDL
ht.count = old ht.count - 1
unset_trace
DB_EXEC_USE
ensure DB_EXEC_USE
trace_status: not is_tracing
feature
append (s: STRING_8)
`s'
STRING_8
require STRING_8
argument_not_void: s /= Void
ensure STRING_8
new_count: count = old count + old s.count
appended: elks_checking implies is_equal (old twin + old s.twin)
append_boolean (b: BOOLEAN)
`b'
STRING_8
append_character (c: CHARACTER_8)
`c'
STRING_8extend
STRING_8
ensure then STRING_8
item_inserted: item (count) = c
new_count: count = old count + 1
stable_before: elks_checking implies substring (1, count - 1).is_equal (old twin)
append_code (c: like code)
`c'
STRING_GENERAL
require STRING_GENERAL
valid_code: valid_code (c)
ensure then STRING_GENERAL
item_inserted: code (count) = c
new_count: count = old count + 1
stable_before: elks_checking implies substring (1, count - 1).is_equal (old twin)
append_double (d: REAL_64)
`d'
STRING_8
append_integer (i: INTEGER_32)
`i'
STRING_8
append_real (r: REAL_32)
`r'
STRING_8
append_string (s: STRING_8)
`s'
STRING_8
ensure STRING_8
appended: s /= Void implies (elks_checking implies is_equal (old twin + old s.twin))
append_string_general (s: STRING_GENERAL)
`s'
STRING_8
require STRING_GENERAL
argument_not_void: s /= Void
compatible_strings: is_string_8 implies s.is_valid_as_string_8
ensure STRING_GENERAL
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)
copy (other: like Current)
`other'
twin
STRING_8
require ANY
other_not_void: other /= Void
type_identity: same_type (other)
ensure ANY
is_equal: is_equal (other)
ensure then STRING_8
new_result_count: count = other.count
extend (c: CHARACTER_8)
`c'
STRING_8append_character
STRING_8
require COLLECTION
extendible: extendible
ensure COLLECTION
item_inserted: is_inserted (c)
ensure then BAG
one_more_occurrence: occurrences (c) = old (occurrences (c)) + 1
ensure then STRING_8
item_inserted: item (count) = c
new_count: count = old count + 1
stable_before: elks_checking implies substring (1, count - 1).is_equal (old twin)
fill (other: CONTAINER [CHARACTER_8])
`other'
`other'
COLLECTION
require COLLECTION
other_not_void: other /= Void
extendible: extendible
fill_blank
capacity
STRING_8
ensure STRING_8
filled: full
same_size: (count = capacity) and (capacity = old capacity)
fill_character (c: CHARACTER_8)
capacity`c'
STRING_8
ensure STRING_8
filled: full
same_size: (count = capacity) and (capacity = old capacity)
fill_with (c: CHARACTER_8)
`c'
STRING_8
ensure STRING_8
same_count: (count = old count) and (capacity >= old capacity)
filled: elks_checking implies occurrences (c) = count
insert_character (c: CHARACTER_8; i: INTEGER_32)
`c'`i'
`i'count
STRING_8
require STRING_8
valid_insertion_index: 1 <= i and i <= count + 1
ensure STRING_8
one_more_character: count = old count + 1
inserted: item (i) = c
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, count))
insert_string (s: STRING_8; i: INTEGER_32)
`s'`i'
`i'count
STRING_8
require STRING_8
string_exists: s /= Void
valid_insertion_index: 1 <= i and i <= count + 1
ensure STRING_8
inserted: elks_checking implies (is_equal (old substring (1, i - 1) + old (s.twin) + old substring (i, count)))
keep_head (n: INTEGER_32)
`n'
`n'count
STRING_8
require STRING_8
non_negative_argument: n >= 0
ensure STRING_8
new_count: count = n.min (old count)
kept: elks_checking implies is_equal (old substring (1, n.min (count)))
keep_tail (n: INTEGER_32)
`n'
`n'count
STRING_8
require STRING_8
non_negative_argument: n >= 0
ensure STRING_8
new_count: count = n.min (old count)
kept: elks_checking implies is_equal (old substring (count - n.min (count) + 1, count))
left_adjust
STRING_8
ensure STRING_8
valid_count: count <= old count
new_count: not is_empty implies not item (1).is_space
kept: elks_checking implies is_equal ((old twin).substring (old count - count + 1, old count))
precede (c: CHARACTER_8)
`c'
STRING_8prepend_character
STRING_8
ensure STRING_8
new_count: count = old count + 1
prepend (s: STRING_8)
`s'
STRING_8
require STRING_8
argument_not_void: s /= Void
ensure STRING_8
new_count: count = old (count + s.count)
inserted: elks_checking implies string.is_equal (old (s.twin) + old substring (1, count))
prepend_boolean (b: BOOLEAN)
`b'
STRING_8
prepend_character (c: CHARACTER_8)
`c'
STRING_8precede
STRING_8
ensure STRING_8
new_count: count = old count + 1
prepend_double (d: REAL_64)
`d'
STRING_8
prepend_integer (i: INTEGER_32)
`i'
STRING_8
prepend_real (r: REAL_32)
`r'
STRING_8
prepend_string (s: STRING_8)
`s'
STRING_8
string_put (c: CHARACTER_8; i: INTEGER_32)
`i'`c'
STRING_8
require TABLE
valid_key: valid_index (i)
require TO_SPECIAL
valid_index: valid_index (i)
ensure then INDEXABLE
insertion_done: item (i) = c
ensure TO_SPECIAL
inserted: item (i) = c
ensure then STRING_8
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))
put_code (v: NATURAL_32; i: INTEGER_32)
`i'`v'
STRING_8
require STRING_GENERAL
valid_code: valid_code (v)
valid_index: valid_index (i)
ensure STRING_GENERAL
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))
replace_blank
STRING_8
ensure STRING_8
same_size: (count = old count) and (capacity >= old capacity)
all_blank: elks_checking implies occurrences (' ') = count
replace_substring (s: STRING_8; start_index, end_index: INTEGER_32)
`start_index'`end_index'`s'
STRING_8
require STRING_8
string_not_void: s /= Void
valid_start_index: 1 <= start_index
valid_end_index: end_index <= count
meaningfull_interval: start_index <= end_index + 1
ensure STRING_8
new_count: count = old count + old s.count - end_index + start_index - 1
replaced: elks_checking implies (is_equal (old (substring (1, start_index - 1) + s + substring (end_index + 1, count))))
replace_substring_all (original, new: like Current)
`original'`new'
STRING_8
require STRING_8
original_exists: original /= Void
new_exists: new /= Void
original_not_empty: not original.is_empty
right_adjust
STRING_8
ensure STRING_8
valid_count: count <= old count
new_count: (count /= 0) implies ((item (count) /= ' ') and (item (count) /= '%T') and (item (count) /= '%R') and (item (count) /= '%N'))
kept: elks_checking implies is_equal ((old twin).substring (1, count))
set (t: like Current; n1, n2: INTEGER_32)
`t'`n1'
`n2'
STRING_8
require STRING_8
argument_not_void: t /= Void
ensure STRING_8
is_substring: is_equal (t.substring (n1, n2))
set_boolean_field (i: INTEGER_32; object: ANY; value: BOOLEAN)
INTERNAL
require 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_32; object: ANY; value: CHARACTER_8)
`i'`object'`value'
INTERNAL
require 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_32; object: ANY; value: REAL_64)
INTERNALset_real_64_field
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
real_64_field: field_type (i, object) = real_64_type
set_integer_16_field (i: INTEGER_32; object: ANY; value: INTEGER_16)
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
integer_16_field: field_type (i, object) = integer_16_type
set_integer_32_field (i: INTEGER_32; object: ANY; value: INTEGER_32)
INTERNALset_integer_field
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
integer_32_field: field_type (i, object) = integer_32_type
set_integer_64_field (i: INTEGER_32; object: ANY; value: INTEGER_64)
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
integer_64_field: field_type (i, object) = integer_64_type
set_integer_8_field (i: INTEGER_32; object: ANY; value: INTEGER_8)
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
integer_8_field: field_type (i, object) = integer_8_type
set_integer_field (i: INTEGER_32; object: ANY; value: INTEGER_32)
INTERNALset_integer_32_field
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
integer_32_field: field_type (i, object) = integer_32_type
set_natural_16_field (i: INTEGER_32; object: ANY; value: NATURAL_16)
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
natural_16_field: field_type (i, object) = natural_16_type
set_natural_32_field (i: INTEGER_32; object: ANY; value: NATURAL_32)
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
natural_32_field: field_type (i, object) = natural_32_type
set_natural_64_field (i: INTEGER_32; object: ANY; value: NATURAL_64)
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
natural_64_field: field_type (i, object) = natural_64_type
set_natural_8_field (i: INTEGER_32; object: ANY; value: NATURAL_8)
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
natural_8_field: field_type (i, object) = natural_8_type
set_pointer_field (i: INTEGER_32; object: ANY; value: POINTER)
INTERNAL
require 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_32_field (i: INTEGER_32; object: ANY; value: REAL_32)
INTERNALset_real_field
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
real_32_field: field_type (i, object) = real_32_type
set_real_64_field (i: INTEGER_32; object: ANY; value: REAL_64)
INTERNALset_double_field
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
real_64_field: field_type (i, object) = real_64_type
set_real_field (i: INTEGER_32; object: ANY; value: REAL_32)
INTERNALset_real_32_field
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
real_32_field: field_type (i, object) = real_32_type
set_reference_field (i: INTEGER_32; object: ANY; value: ANY)
INTERNAL
require 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
value_conforms_to_field_static_type: value /= Void implies type_conforms_to (dynamic_type (value), field_static_type_of_type (i, dynamic_type (object)))
share (other: STRING_8)
`other'
`other'
STRING_8
require STRING_8
argument_not_void: other /= Void
ensure STRING_8
shared_count: other.count = count
shared_area: other.area = area
subcopy (other: like Current; start_pos, end_pos, index_pos: INTEGER_32)
`other'`start_pos'
`end_pos'`index_pos'
STRING_8
require STRING_8
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)
ensure STRING_8
same_count: count = old count
copied: elks_checking implies (is_equal (old substring (1, index_pos - 1) + old other.substring (start_pos, end_pos) + old substring (index_pos + (end_pos - start_pos + 1), count)))
infix "+" (s: STRING_8): like Current
STRING_8
require STRING_8
argument_not_void: s /= Void
ensure STRING_8
result_exists: Result /= Void
new_count: Result.count = count + s.count
initial: elks_checking implies Result.substring (1, count).is_equal (Current)
final: elks_checking implies Result.substring (count + 1, count + s.count).same_string (s)
feature
prune (c: CHARACTER_8)
`c'
STRING_8
require COLLECTION
prunable: prunable
require else STRING_8
True
prune_all (c: CHARACTER_8)
`c'
STRING_8
require COLLECTION
prunable: prunable
require else STRING_8
True
ensure COLLECTION
no_more_occurrences: not has (c)
ensure then STRING_8
changed_count: count = (old count) - (old occurrences (c))
prune_all_leading (c: CHARACTER_8)
`c'
STRING_8
prune_all_trailing (c: CHARACTER_8)
`c'
STRING_8
remove (i: INTEGER_32)
`i'
STRING_8
require STRING_GENERAL
valid_index: valid_index (i)
ensure STRING_GENERAL
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)
remove_head (n: INTEGER_32)
`n'
`n'count
STRING_8
require STRING_8
n_non_negative: n >= 0
ensure STRING_8
removed: elks_checking implies is_equal (old substring (n.min (count) + 1, count))
remove_substring (start_index, end_index: INTEGER_32)
`start_index'
`end_index'
STRING_8
require STRING_8
valid_start_index: 1 <= start_index
valid_end_index: end_index <= count
meaningful_interval: start_index <= end_index + 1
ensure STRING_8
removed: elks_checking implies is_equal (old substring (1, start_index - 1) + old substring (end_index + 1, count))
remove_tail (n: INTEGER_32)
`n'
`n'count
STRING_8
require STRING_8
n_non_negative: n >= 0
ensure STRING_8
removed: elks_checking implies is_equal (old substring (1, count - n.min (count)))
wipe_out
STRING_8
require COLLECTION
prunable: prunable
ensure COLLECTION
wiped_out: is_empty
ensure then STRING_8
is_empty: count = 0
empty_capacity: capacity = 0
feature
adapt_size
count
STRING_8
automatic_grow
Growth_percentage
RESIZABLE
ensure RESIZABLE
increased_capacity: capacity >= old capacity + old capacity * growth_percentage // 100
grow (newsize: INTEGER_32)
`newsize'
STRING_8
ensure RESIZABLE
new_capacity: capacity >= newsize
resize (newsize: INTEGER_32)
`newsize'
STRING_8
require STRING_GENERAL
new_size_non_negative: newsize >= 0
feature
as_lower: like Current
STRING_8
ensure STRING_8
length: Result.count = count
anchor: count > 0 implies Result.item (1) = item (1).as_lower
recurse: count > 1 implies Result.substring (2, count).is_equal (substring (2, count).as_lower)
as_string_32: STRING_32
`Current'
STRING_GENERALto_string_32
STRING_GENERAL
ensure STRING_GENERAL
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'
STRING_GENERAL
ensure STRING_GENERAL
as_string_8_not_void: Result /= Void
identity: (is_string_8 and Result = Current) or (not is_string_8 and Result /= Current)
as_upper: like Current
STRING_8
ensure STRING_8
length: Result.count = count
anchor: count > 0 implies Result.item (1) = item (1).as_upper
recurse: count > 1 implies Result.substring (2, count).is_equal (substring (2, count).as_upper)
boolean_format (object: BOOLEAN): STRING_8
`object'
DB_FORMAT
center_justify
count
STRING_8
character_justify (pivot: CHARACTER_8; position: INTEGER_32)
`pivot'
`position'
STRING_8
require STRING_8
valid_position: position <= capacity
positive_position: position >= 1
pivot_not_space: pivot /= ' '
not_empty: not is_empty
charconv (i: INTEGER_32): CHARACTER_8
`i'
BASIC_ROUTINES
date_format (object: DATE_TIME): STRING_8
`object'
DB_FORMAT
require DB_FORMAT
argument_not_void: object /= Void
left_justify
count
STRING_8
linear_representation: LINEAR [CHARACTER_8]
STRING_8
mirror
STRING_8
ensure STRING_8
same_count: count = old count
mirrored: like Current
STRING_8
ensure STRING_8
same_count: Result.count = count
right_justify
count
STRING_8
ensure STRING_8
same_count: count = old count
split (a_separator: CHARACTER_8): LIST [STRING_8]
`a_separator'
STRING_8
ensure STRING_8
Result /= Void
string_format (object: STRING_8): STRING_8
`object'
DB_FORMAT
require DB_FORMAT
argument_not_void: object /= Void
to_boolean: BOOLEAN
`True'`False'
STRING_8
require STRING_8
is_boolean: string_is_boolean
ensure STRING_8
to_boolean: (Result = true_constant.same_string (as_lower)) or (not Result = false_constant.same_string (as_lower))
frozen to_c: ANY
STRING_8
require STRING_8
not_is_dotnet: not {PLATFORM}.is_dotnet
frozen to_cil: SYSTEM_STRING
`1'count
STRING_GENERAL
require STRING_GENERAL
is_dotnet: {PLATFORM}.is_dotnet
ensure STRING_GENERAL
to_cil_not_void: Result /= Void
to_double: REAL_64
STRING_8
require STRING_8
represents_a_double: string_is_double
to_integer: INTEGER_32
STRING_8to_integer_32
STRING_8
require STRING_8
is_integer: is_integer_32
to_integer_16: INTEGER_16
STRING_8
require STRING_8
is_integer_16: is_integer_16
to_integer_32: INTEGER_32
STRING_8to_integer
STRING_8
require STRING_8
is_integer: is_integer_32
to_integer_64: INTEGER_64
STRING_8
require STRING_8
is_integer_64: is_integer_64
to_integer_8: INTEGER_8
STRING_8
require STRING_8
is_integer_8: is_integer_8
to_lower
STRING_8
ensure STRING_8
length_end_content: elks_checking implies is_equal (old as_lower)
to_natural: NATURAL_32
STRING_8to_natural_32
STRING_8
require STRING_8
is_natural: is_natural
to_natural_16: NATURAL_16
STRING_8
require STRING_8
is_natural_16: is_natural_16
to_natural_32: NATURAL_32
STRING_8to_natural
STRING_8
require STRING_8
is_natural: is_natural
to_natural_64: NATURAL_64
STRING_8
require STRING_8
is_natural_64: is_natural_64
to_natural_8: NATURAL_8
STRING_8
require STRING_8
is_natural_8: is_natural_8
to_real: REAL_32
STRING_8
require STRING_8
represents_a_real: string_is_real
to_string_32: STRING_32
`Current'
STRING_GENERALas_string_32
STRING_GENERAL
ensure STRING_GENERAL
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'
STRING_GENERAL
require STRING_GENERAL
is_valid_as_string_8: is_valid_as_string_8
ensure STRING_GENERAL
as_string_8_not_void: Result /= Void
identity: (is_string_8 and Result = Current) or (not is_string_8 and Result /= Current)
to_upper
STRING_8
ensure STRING_8
length_end_content: elks_checking implies is_equal (old as_upper)
feature
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)
multiply (n: INTEGER_32)
STRING_8
require STRING_8
meaningful_multiplier: n >= 1
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'
STRING_8
require STRING_GENERAL
True
ensure STRING_GENERAL
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))
ensure then STRING_8
first_item: Result.count > 0 implies Result.item (1) = item (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
abs (n: INTEGER_32): INTEGER_32
`n'
BASIC_ROUTINES
ensure BASIC_ROUTINES
non_negative_result: Result >= 0
bottom_int_div (n1, n2: INTEGER_32): INTEGER_32
`n1'`n2'
BASIC_ROUTINES
deep_traversal (object: ANY)
`object'
EXT_INTERNAL
require EXT_INTERNAL
root_object_non_void: object /= Void
frozen default: like Current
ANY
frozen default_pointer: POINTER
`POINTER'
`p'default
`p'`POINTER'
ANY
default_rescue
ANY
frozen do_nothing
ANY
field_clean (i: INTEGER_32; object: ANY): BOOLEAN
`i'`object'
EXT_INTERNAL
require EXT_INTERNAL
object_not_void: object /= Void
field_copy (i: INTEGER_32; object, value: ANY): BOOLEAN
`value'`i'`object'
EXT_INTERNAL
require EXT_INTERNAL
object_not_void: object /= Void
value_not_void: value /= Void
force (obj: ANY)
`object'
require
object_exists: obj /= Void
owns_repository: owns_repository
repository_exists: repository.exists
get_complex_value (obj: ANY; str: STRING_8)
`obj'`str'
SQL_SCAN
require SQL_SCAN
object_exists: obj /= Void
str_exists: str /= Void
get_value (obj: ANY; str: STRING_8)
`obj'`str'
SQL_SCAN
require SQL_SCAN
str_exists: str /= Void
object_finish_action (object: ANY)
EXT_INTERNAL
object_init_action (object: ANY)
EXT_INTERNAL
parse (s: STRING_8): STRING_8
`s'
SQL_SCAN
put (object: ANY)
`object'
require
object_exists: object /= Void
owns_repository: owns_repository
repository_exists: repository.exists
reference_object_action (i: INTEGER_32; object: ANY)
EXT_INTERNAL
replace
`ht.item (":key")'
SQL_SCAN
rsign (r: REAL_32): INTEGER_32
`r'
`r'
`r'
`r'
BASIC_ROUTINES
ensure BASIC_ROUTINES
correct_negative: (r < 0) = (Result = -1)
correct_zero: (r = 0) = (Result = 0)
correct_positive: (r > 0) = (Result = 1)
sign (n: INTEGER_32): INTEGER_32
`n'
`n'
`n'
`n'
BASIC_ROUTINES
ensure 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_32; object: ANY)
EXT_INTERNAL
store_action (object: ANY)
EXT_INTERNAL
switch_mark (obj: ANY)
`obj'
EXT_INTERNAL
require EXT_INTERNAL
object_not_void: obj /= Void
traversal (object: ANY)
`obj'
EXT_INTERNAL
require EXT_INTERNAL
object_not_void: object /= Void
unmark_structure (obj: ANY)
EXT_INTERNAL
require EXT_INTERNAL
object_not_void: obj /= Void
up_int_div (n1, n2: INTEGER_32): INTEGER_32
`n1'`n2'
BASIC_ROUTINES
feature
is_instance_of (object: ANY; type_id: INTEGER_32): BOOLEAN
`object'`type_id'
INTERNAL
require INTERNAL
object_not_void: object /= Void
type_id_nonnegative: type_id >= 0
type_conforms_to (type1, type2: INTEGER_32): BOOLEAN
`type1'`type2'
INTERNAL
require INTERNAL
type1_nonnegative: type1 >= 0
type2_nonnegative: type2 >= 0
feature
mismatch_information: MISMATCH_INFORMATION
MISMATCH_CORRECTOR
feature
dynamic_type_from_string (class_type: STRING_8): INTEGER_32
`class_type'
INTERNAL
require INTERNAL
class_type_not_void: class_type /= Void
class_type_not_empty: not class_type.is_empty
is_valid_type_string: is_valid_type_string (class_type)
ensure INTERNAL
dynamic_type_from_string_valid: Result = -1 or Result = none_type or Result >= 0
new_instance_of (type_id: INTEGER_32): ANY
`type_id'
`type_id'
new_special_any_instance
INTERNAL
require INTERNAL
type_id_nonnegative: type_id >= 0
not_special_type: not is_special_type (type_id)
ensure INTERNAL
not_special_type: not is_special (Result)
dynamic_type_set: dynamic_type (Result) = type_id
new_special_any_instance (type_id, count: INTEGER_32): SPECIAL [ANY]
`type_id'
count
`SPECIAL'
INTERNAL
require INTERNAL
count_valid: count >= 0
type_id_nonnegative: type_id >= 0
special_type: is_special_any_type (type_id)
ensure INTERNAL
special_type: is_special (Result)
dynamic_type_set: dynamic_type (Result) = type_id
count_set: Result.count = count
feature
lock_marking
markunmarkmark
unmark
INTERNAL
mark (obj: ANY)
`obj'
lock_marking
INTERNAL
require INTERNAL
object_not_void: obj /= Void
object_not_marked: not is_marked (obj)
ensure INTERNAL
is_marked: is_marked (obj)
unlock_marking
markunmark
markunmark
INTERNAL
unmark (obj: ANY)
`obj'
lock_marking
INTERNAL
require INTERNAL
object_not_void: obj /= Void
object_marked: is_marked (obj)
ensure INTERNAL
is_not_marked: not is_marked (obj)
feature
io: STD_FILES
ANY
out: STRING_8
STRING_8
require ANY
True
ensure then STRING_8
out_not_void: Result /= Void
same_items: same_type ("") implies Result.same_string (Current)
print (some: ANY)
`some'
ANY
frozen tagged_out: STRING_8
ANYout
ANY
feature
operating_environment: OPERATING_ENVIRONMENT
ANY
feature
compiler_version: INTEGER_32
INTERNAL
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
STRING_8
extendible: extendible
compare_character: not object_comparison
index_set_has_same_count: index_set.count = count
area_not_void: area /= Void
COMPARABLE
irreflexive_comparison: not (Current < Current)
INDEXABLE
index_set_not_void: index_set /= Void
RESIZABLE
increase_by_at_least_one: minimal_increase >= 1
BOUNDED
valid_count: count <= capacity
full_definition: full = (count = capacity)
FINITE
empty_definition: is_empty = (count = 0)
non_negative_count: count >= 0
indexing
copyright: "Copyright (c) 1984-2006, Eiffel Software and others"
license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
source: "[
Eiffel Software
356 Storke Road, Goleta, CA 93117 USA
Telephone 805-685-1006, Fax 805-685-6869
Website http://www.eiffel.com
Customer support http://support.eiffel.com
]"
end DATABASE_STORE