indexing
description: "Implementation of DB_ALL_TYPES"
legal: "See notice at end of class."
status: "See notice at end of class."
date: "$Date: 2006-12-21 11:51:40 -0800 (Thu, 21 Dec 2006) $"
revision: "$Revision: 65703 $"
class interface
DATABASE_ALL_TYPES [G -> DATABASE create default_create end]
create
make
feature
accommodate (n: INTEGER_32)
`n'
HASH_TABLE
require HASH_TABLE
n >= 0
ensure HASH_TABLE
count_not_changed: count = old count
slot_count_same_as_count: used_slot_count = count
breathing_space: count < capacity
make
ht_make (n: INTEGER_32)
`n'
`n'
HASH_TABLE
ensure HASH_TABLE
breathing_space: n < capacity
more_than_minimum: capacity > minimum_capacity
no_status: not special_status
feature
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_field (i: INTEGER_32; object: ANY): CHARACTER_32
`i'`object'
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
character_32_field: field_type (i, object) = character_32_type
character_32_type: INTEGER_32 is 12
INTERNALWide_character_type
INTERNAL
character_8_field (i: INTEGER_32; object: ANY): CHARACTER_8
`i'`object'
INTERNALcharacter_field
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
character_8_field: field_type (i, object) = character_8_type
character_8_type: INTEGER_32 is 2
INTERNALCharacter_type
INTERNAL
character_field (i: INTEGER_32; object: ANY): CHARACTER_8
`i'`object'
INTERNALcharacter_8_field
INTERNAL
require INTERNAL
object_not_void: object /= Void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
character_8_field: field_type (i, object) = character_8_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
current_keys: ARRAY [INTEGER_32]
count
HASH_TABLE
ensure HASH_TABLE
good_count: Result.count = count
cursor: CURSOR
HASH_TABLE
ensure HASH_TABLE
cursor_not_void: Result /= Void
db_type (object: ANY): DB_TYPE
`object'
ensure
result_value: Result = item (dynamic_type (object))
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
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
found_item: DB_TYPE
HASH_TABLE
generating_type: STRING_8
ANY
ensure ANY
generating_type_not_void: Result /= Void
generating_type_not_empty: not Result.is_empty
generator: STRING_8
ANY
ensure ANY
generator_not_void: Result /= Void
generator_not_empty: not Result.is_empty
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
has (key: INTEGER_32): BOOLEAN
`key'
HASH_TABLE
ensure then HASH_TABLE
default_case: (key = computed_default_key) implies (Result = has_default)
has_item (v: DB_TYPE): BOOLEAN
`v'
object_comparison
HASH_TABLE
ensure CONTAINER
not_found_in_empty: Result implies not is_empty
has_key (key: INTEGER_32): BOOLEAN
`key'found_item
HASH_TABLE
ensure then HASH_TABLE
default_case: (key = computed_default_key) implies (Result = has_default)
found: Result = found
item_if_found: found implies (found_item = item (key))
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 alias "[]" (key: INTEGER_32): DB_TYPE assign put
`key'
`G'
HASH_TABLEinfix "@"
HASH_TABLE
require TABLE
valid_key: valid_key (key)
ensure then HASH_TABLE
default_value_if_not_present: (not (has (key))) implies (Result = computed_default_value)
item_for_iteration: DB_TYPE
HASH_TABLE
require HASH_TABLE
not_off: not off
key_for_iteration: INTEGER_32
HASH_TABLE
require HASH_TABLE
not_off: not off
ensure HASH_TABLE
at_iteration_position: Result = key_at (iteration_position)
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
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 "@" (key: INTEGER_32): DB_TYPE assign put
`key'
`G'
HASH_TABLEitem
HASH_TABLE
require TABLE
valid_key: valid_key (key)
ensure then HASH_TABLE
default_value_if_not_present: (not (has (key))) implies (Result = computed_default_value)
feature
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
HASH_TABLE
count: INTEGER_32
HASH_TABLE
deep_physical_size (object: ANY): INTEGER_32
`object'
INTERNAL
require INTERNAL
object_not_void: object /= Void
field_count (object: ANY): INTEGER_32
`object'
INTERNAL
require IN