+
Point of view
WHEN_ITEM
class WHEN_ITEM_2
specialize_in (new_type:
TYPE): WHEN_ITEM_2
effective function
require
ensure
- Result.has_been_specialized
require
- parent_type /= Void
- parent_edge /= Void
- new_type /= Void
- new_type /= parent_type
- has_been_specialized
ensure
- has_been_specialized
- Result.has_been_specialized
specialize_2_character (type:
TYPE): WHEN_ITEM_2
effective function
require
ensure
- has_been_specialized
- Result.has_been_specialized
specialize_2_integer (type:
TYPE): WHEN_ITEM_2
effective function
require
ensure
- has_been_specialized
- Result.has_been_specialized
specialize_2_string (type:
TYPE): WHEN_ITEM_2
effective function
require
ensure
- has_been_specialized
- Result.has_been_specialized
inspect ... when foo .. bar, then ...