+
Point of view
LIVE_TYPE
class CLASS_INVARIANT
compile_to_c (type:
TYPE)
effective procedure
define_check_invariant_c_function (current_type:
LIVE_TYPE)
effective procedure
require
- current_type /= Void
- current_type.at_run_time
specialize_in (type:
TYPE): CLASS_INVARIANT
frozen
effective function
frozen
effective function
require
- parent_type /= Void
- parent_edge /= Void
- new_type /= Void
- new_type /= parent_type
- has_been_specialized
ensure
specialize_2 (type:
TYPE): CLASS_INVARIANT
frozen
effective function
frozen
effective function
ensure
-
assertion_check_only: Result
frozen
effective function
frozen
effective function
frozen
effective procedure
safety_check (type:
TYPE)
frozen
effective procedure
simplify (type:
TYPE): CLASS_INVARIANT
frozen
effective function
adapt_for (type:
TYPE): CLASS_INVARIANT
frozen
effective function
frozen
effective procedure
frozen
effective function