+
Point of view
EXTERNAL_ROUTINE
class EXTERNAL_PROCEDURE
require
- target_type.direct_non_void_call_flag
frozen
effective function
frozen
effective procedure
ensure
- rescue_compound = instruction
frozen
effective function
specialize_body_in (new_type:
TYPE, can_twin:
BOOLEAN): EXTERNAL_PROCEDURE
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): EXTERNAL_PROCEDURE
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
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
frozen
effective function