+
Point of view
INTERNALS_HANDLER
deferred class BACKTRACKING_NODE_BINARY
-
first_not_void: first /= Void
-
second_not_void: second /= Void
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