+
Point of view
All features
class NATIVE_ARRAY_INTERNALS [E_]
Summary
NATIVE_ARRAY_INTERNALS plays the same role as TYPED_INTERNALS, except they describe NATIVE_ARRAY's.
Direct parents
Inherit list: TYPED_INTERNALS
Class invariant
Overview
Creation features
{}
{INTERNALS_HANDLER}
  • make_blank (capacity_: INTEGER_32)
    Attach Current to a blank object: all items of the object have their default value (references are Void, INTEGERs are 0, BOOLEANs are False, etc)
Features
Getting information about the described object's type
{INTERNALS_HANDLER, INTERNALS}
{INTERNALS_HANDLER}
  • for_object (native_array: NATIVE_ARRAY[ANY], capacity_: INTEGER_32)
    Attach Current to native_array
  • make_blank (capacity_: INTEGER_32)
    Attach Current to a blank object: all items of the object have their default value (references are Void, INTEGERs are 0, BOOLEANs are False, etc)
Getting information about the type's attributes
{INTERNALS_HANDLER}
Accessing the object's attributes
{INTERNALS_HANDLER}
Getting information about the described object's type
{INTERNALS_HANDLER, INTERNALS}
{INTERNALS_HANDLER}
{INTERNALS_HANDLER}
  • object: E_
    The object Current is attached to
{TYPED_INTERNALS}
{ANY}
{}
Accessing the object's attributes
{INTERNALS_HANDLER}
type_is_native_array: BOOLEAN
is True
constant attribute
Is the type described by Current a NATIVE_ARRAY?
ensure
  • Result = type_generator.is_equal("NATIVE_ARRAY")
type_attribute_is_expanded (i: INTEGER_32): BOOLEAN
effective function
Is the type of the ith attribute expanded?
require
  • i.in_range(1, type_attribute_count)
type_item_is_expanded: BOOLEAN
type_can_be_assigned_to_attribute (other: INTERNALS, i: INTEGER_32): BOOLEAN
effective function
Can the object attached to other be assigned to the ith attribute?
require
  • i.in_range(1, type_attribute_count)
ensure
  • other = Void implies Result = not type_attribute_is_expanded(i)
type_can_be_assigned_to_item (other: INTERNALS): BOOLEAN
for_object (native_array: NATIVE_ARRAY[ANY], capacity_: INTEGER_32)
effective procedure
Attach Current to native_array
require ensure
make_blank (capacity_: INTEGER_32)
Attach Current to a blank object: all items of the object have their default value (references are Void, INTEGERs are 0, BOOLEANs are False, etc)
ensure
type_attribute_count: INTEGER_32
Number of attributes of the type described by Current
ensure
capacity: INTEGER_32
writable attribute
type_attribute_name (i: INTEGER_32): STRING
effective function
Name of the ith attribute of the type described by Current.
require
  • i.in_range(1, type_attribute_count)
ensure
  • Result /= Void
type_attribute_generator (i: INTEGER_32): STRING
effective function
Name of the base class of the ith attribute of the type described by Current.
require
  • i.in_range(1, type_attribute_count)
ensure
  • Result /= Void
type_item_generator: STRING
type_attribute_generating_type (i: INTEGER_32): STRING
effective function
Name of the type of the ith attribute of the type described by Current.
require
  • i.in_range(1, type_attribute_count)
ensure
  • Result /= Void
type_item_generating_type: STRING
object_attribute (i: INTEGER_32): INTERNALS
Read the ith attribute of the type described by Current (also see type_attribute).
If this attribute is attached to an object, then Result is also attached to that object
require
  • i.in_range(1, type_attribute_count)
ensure
  • type_attribute_is_expanded(i) implies Result /= Void
set_object_attribute (element: INTERNALS, i: INTEGER_32)
Write the ith attribute of the type described by Current
require
  • i.in_range(1, type_attribute_count)
  • type_can_be_assigned_to_attribute(element, i)
  • object_can_be_modified
ensure
  • element = Void implies object_attribute(i) = Void
  • element /= Void implies object_attribute(i).is_equal(element)
Name of the base class of the type described by Current.
For instance, if Current is a TYPED_INTERNALS[ARRAY[INTEGER]], type_generator is "ARRAY".
type_generating_type: STRING
Name of the type described by Current.
For instance, if Current is a TYPED_INTERNALS[ARRAY[INTEGER]], type_generating_type is "ARRAY[INTEGER]".
type_is_expanded: BOOLEAN
Is the type described by Current expanded?
object_as_pointer: POINTER
Pointer to the object currently attached to Current.
require
  • type_is_expanded implies type_generator.is_equal("NATIVE_ARRAY")
ensure
  • Result.is_not_null
object: E_
effective function
The object Current is attached to
require ensure
object_memory: E_
writable attribute
is_equal (other: NATIVE_ARRAY_INTERNALS [E_]): BOOLEAN
{ANY}
Is other attached to an object considered equal to current object?
require
  • other /= Void
ensure
  • commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)
set_object_can_be_retrieved
effective procedure
{ANY}
Forbid further modification of the object through set_object_attribute, so that it can safely be released into the system.
Note that the embedded object is notified via its internals_can_be_retrieved feature.
ensure
  • object_can_be_retrieved
correct_generating_type (object_: E_): BOOLEAN
effective function
{}
ensure
object_can_be_retrieved: BOOLEAN
writable attribute
Can the object be retrieved by the rest of the system through object?
object_can_be_modified: BOOLEAN
effective function
Can the object be modified through set_object_attribute, i.e.
is it safely isolated from the rest of the system?
ensure