home
wiki
classes/clusters list
class information
+
Point of view
ANY
ANY
INTERNALS_HANDLER
All features
class BACKTRACKING_NODE_OR_LIST
Summary
top
Node for an alternative of list of nodes
Direct parents
inherit list:
BACKTRACKING_NODE_LIST
Class invariant
top
node_not_void:
node /= Void
Overview
top
creation features
exported features
explore
(explorer:
BACKTRACKING
)
That feature must update the state of 'explorer'.
node
:
BACKTRACKING_NODE
first node of the list
next
: BACKTRACKING_NODE_OR_LIST
remaining of the list
make
(nod:
BACKTRACKING_NODE
, nxt: BACKTRACKING_NODE_OR_LIST)
set_node
(value:
BACKTRACKING_NODE
)
set_next
(value: BACKTRACKING_NODE_OR_LIST)
explore
(explorer:
BACKTRACKING
)
effective procedure
top
That feature must update the state of 'explorer'.
node
:
BACKTRACKING_NODE
writable attribute
top
first node of the list
next
: BACKTRACKING_NODE_OR_LIST
writable attribute
top
remaining of the list
make
(nod:
BACKTRACKING_NODE
, nxt: BACKTRACKING_NODE_OR_LIST)
effective procedure
top
require
value_not_void:
nod /= Void
ensure
definition:
node
= nod and
next
= nxt
node_not_void:
node
/= Void
set_node
(value:
BACKTRACKING_NODE
)
effective procedure
top
require
value_not_void:
value /= Void
ensure
definition:
node
= value
node_not_void:
node
/= Void
set_next
(value: BACKTRACKING_NODE_OR_LIST)
effective procedure
top
ensure
definition:
next
= value