+
Point of view
All features
class BACKTRACKING_NODE_AND_PAIR
-
first_not_void: first /= Void
-
second_not_void: second /= Void
do_fill_tagged_out_memory
effective procedure
{}
require
-
first_not_void: frst /= Void
-
second_not_void: scnd /= Void
ensure
require
-
value_not_void: value /= Void
ensure
-
definition: first = value
-
first_not_void: first /= Void
require
-
value_not_void: value /= Void
ensure
require
-
locked: tagged_out_locked
ensure
-
still_locked: tagged_out_locked
fill_tagged_out_memory_flag:
BOOLEAN
writable attribute
{}