+
Point of view
WHEN_ITEM_1
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
validity_check_continued_when_item_1 (occurrence_2:
WHEN_ITEM_1)
effective procedure
inspect ... when foo .. bar, then ...