+
Point of view
INTERNALS_HANDLER
class DEFERRED_FUNCTION
frozen
effective function
require
- target_type.direct_non_void_call_flag
frozen
effective function
frozen
effective procedure
ensure
- rescue_compound = instruction
specialize_body_in (new_type:
TYPE, can_twin:
BOOLEAN): DEFERRED_FUNCTION
effective function
require
ensure
- not can_twin implies Result = Current
- Result.has_been_specialized
specialize_body_thru (parent_type:
TYPE, parent_edge:
PARENT_EDGE, new_type:
TYPE, can_twin:
BOOLEAN): DEFERRED_FUNCTION
effective function
require
- parent_type /= Void
- parent_edge /= Void
- new_type /= Void
- has_been_specialized
ensure
- not can_twin implies Result = Current
- has_been_specialized
- Result.has_been_specialized
specialize_2 (type:
TYPE): DEFERRED_FUNCTION
effective function
require
ensure
- has_been_specialized
- Result.has_been_specialized
frozen
effective function
class_text_name:
CLASS_NAME
frozen
effective function
frozen
effective function
frozen
effective function
frozen
effective procedure
frozen
effective procedure
frozen
effective function