+
Point of view
PROC_CALL_1
deferred class EXTERNAL_ROUTINE
frozen
effective function
frozen
effective procedure
ensure
- rescue_compound = instruction
frozen
effective function
specialize_body_in (new_type:
TYPE, can_twin:
BOOLEAN): EXTERNAL_ROUTINE
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_ROUTINE
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
require
- target_type.direct_non_void_call_flag
require
- type /= Void
- target /= Void
- target_type /= Void
- arg /= Void
ensure
- Result /= Void implies Result.is_instruction_holder