class NATIVE_ARRAY_INTERNALS [E_]

All features

WARNING: This interface is tentative and may change to a large extent from SmartEiffel 2.2 to SmartEiffel 2.3.

NATIVE_ARRAY_INTERNALS play the same role as TYPED_INTERNALS, except they describe NATIVE_ARRAYs.

Direct parents

conformant parents

TYPED_INTERNALS

Summary

creation features

Actual creation is performed by ANY.to_internals

exported features

Getting information about the described object's type

Getting information about the type's attributes

Accessing the object's attributes

Getting information about the described object's type

Accessing the object's attributes

Details

for_object (native_array: NATIVE_ARRAY[E_], capacity_: INTEGER)

Attach Current to native_array

require

  • native_array.is_not_null
  • native_array.generating_type = type_generating_type

ensure

  • object_can_be_retrieved
  • object = native_array
  • capacity = capacity_

make_blank (capacity_: INTEGER)

Attach Current to a blank object: all items of the object have their default value (references are Void, INTEGERS are 0, BOOLEANs are False...)

ensure

  • object_can_be_modified
  • capacity = capacity_

for_object (object_: E_)

Attach Current to object_

require

  • object_ /= Void
  • object_.generating_type = type_generating_type
  • not type_generator.is_equal(once "NATIVE_ARRAY")

ensure

  • object_can_be_retrieved
  • object = object_

make_blank

Attach Current to a blank object: all attributes of the object have their default value (references are Void, INTEGERS are 0, BOOLEANs are False...)

require

  • not type_generator.is_equal(once "NATIVE_ARRAY")

ensure

  • object_can_be_modified

type_is_native_array: BOOLEAN

Is the type described by Current a NATIVE_ARRAY?

ensure

  • Result = type_generator.is_equal(once "NATIVE_ARRAY")

type_attribute_is_expanded (i: INTEGER): BOOLEAN

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): BOOLEAN

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[E_], capacity_: INTEGER)

Attach Current to native_array

require

  • native_array.is_not_null
  • native_array.generating_type = type_generating_type

ensure

  • object_can_be_retrieved
  • object = native_array
  • capacity = capacity_

make_blank (capacity_: INTEGER)

Attach Current to a blank object: all items of the object have their default value (references are Void, INTEGERS are 0, BOOLEANs are False...)

ensure

  • object_can_be_modified
  • capacity = capacity_

type_attribute_count: INTEGER

Number of attributes of the type described by Current

ensure

  • Result = capacity or Result = 0

capacity: INTEGER
type_attribute_name (i: INTEGER): STRING

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): STRING

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): STRING

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): 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)

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)

type_generator: STRING

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?

for_object (object_: E_)

Attach Current to object_

require

  • object_ /= Void
  • object_.generating_type = type_generating_type
  • not type_generator.is_equal(once "NATIVE_ARRAY")

ensure

  • object_can_be_retrieved
  • object = object_

make_blank

Attach Current to a blank object: all attributes of the object have their default value (references are Void, INTEGERS are 0, BOOLEANs are False...)

require

  • not type_generator.is_equal(once "NATIVE_ARRAY")

ensure

  • object_can_be_modified

object_as_pointer: POINTER

Pointer to the object currently attached to Current.

require

  • type_is_expanded implies type_generator.is_equal(once "NATIVE_ARRAY")

ensure

  • Result.is_not_null

object: E_

The object Current is attached to

require

  • object_can_be_retrieved

ensure

  • Result.generating_type = type_generating_type

object_memory: E_
is_equal (other: NATIVE_ARRAY_INTERNALS [E_]): BOOLEAN

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)

object_can_be_retrieved: BOOLEAN

Can the object be retrieved by the rest of the system through object?

object_can_be_modified: BOOLEAN

Can the object be modified through set_object_attribute, i.e. is it safely isolated from the rest of the system?

ensure

  • Result = not object_can_be_retrieved

set_object_can_be_retrieved

Forbid further modification of the object through set_object_attribute, so that it can safely be released into the system

ensure

  • object_can_be_retrieved

Class invariant