+
Point of view
All features
deferred class BACKTRACKING
- current_continuation = Void or current_continuation = top_sequence
- top_sequence = Void implies current_continuation = Void
require
-
node_not_void: node /= Void
require
-
list_not_void: list /= Void
require
-
node_not_void: node /= Void
require
-
list_not_void: list /= Void
ensure
-
no_solution_when_cleared: Result implies is_off
require
-
sequence_not_void: sequence /= Void
ensure
require
-
alternative_not_void: alternative /= Void
ensure