+
Point of view
All features
class BACKTRACKING_NODE_UNDER_CUT_POINT
-
node_not_void: node /= Void
do_fill_tagged_out_memory
effective procedure
{}
require
-
value_not_void: value /= Void
ensure
-
definition: node = value
-
node_not_void: node /= Void
require
-
value_not_void: value /= Void
ensure
-
definition: node = value
-
node_not_void: node /= Void
require
-
locked: tagged_out_locked
ensure
-
still_locked: tagged_out_locked
fill_tagged_out_memory_flag:
BOOLEAN
writable attribute
{}