+
Point of view
All features
expanded class REPOSITORY_TRANSIENT
require
- not transient_object.type_is_expanded
- transient_object.object_as_pointer /= default_pointer
- not transient_reference.is_empty
- not has_object(transient_reference)
ensure
unregister (transient_reference:
STRING)
effective procedure
require
- not a_object.type_is_expanded
- a_object.object_as_pointer /= default_pointer
ensure
- Result /= Void implies not Result.is_empty
- Result /= Void implies a_object.object_as_pointer = object(Result).object_as_pointer
require
ensure
- Result implies not type.has_prefix("NATIVE_ARRAY")
require
ensure
- Result /= Void
- Result.object_can_be_modified
valid_generating_type_for_native_array_internals (type:
STRING):
BOOLEAN
frozen
{}
require
ensure
- Result implies type.has_prefix("NATIVE_ARRAY")
require
ensure
- Result /= Void
- Result.object_can_be_modified