GNU
|
Liberty Eiffel
|
Automated Tests
|
Wiki
|
Savannah project
|
Debian packages
|
Documentation
>
libraries
>
BACKTRACKING_NODE_LIST
+
Point of view
All features
ANY
All features
deferred class BACKTRACKING_NODE_LIST
Summary
top
Node for a sequence of list of nodes
Direct parents
Inherit list:
BACKTRACKING_NODE
Insert list:
BACKTRACKING_NODE_FILL
Known children
Inherit list:
BACKTRACKING_NODE_AND_LIST
,
BACKTRACKING_NODE_OR_LIST
Class invariant
top
node_not_void:
node
/= Void
Overview
top
Features
{
ANY
}
node
:
BACKTRACKING_NODE
first node of the list
next
: BACKTRACKING_NODE_LIST
remaining of the list
make
(nod:
BACKTRACKING_NODE
, nxt: BACKTRACKING_NODE_LIST)
set_node
(value:
BACKTRACKING_NODE
)
set_next
(value: BACKTRACKING_NODE_LIST)
{
ANY
}
explore
(explorer:
BACKTRACKING
)
That feature must update the state of 'explorer'.
{
ANY
}
fill_tagged_out_memory
Append a viewable information in
tagged_out_memory
in order to affect the behavior of
out
,
tagged_out
, etc.
{}
fill_tagged_out_memory_flag
:
BOOLEAN
do_fill_tagged_out_memory
node
:
BACKTRACKING_NODE
writable attribute
{
ANY
}
top
first node of the list
next
: BACKTRACKING_NODE_LIST
writable attribute
{
ANY
}
top
remaining of the list
make
(nod:
BACKTRACKING_NODE
, nxt: BACKTRACKING_NODE_LIST)
effective procedure
{
ANY
}
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
{
ANY
}
top
require
value_not_void:
value /= Void
ensure
definition:
node
= value
node_not_void:
node
/= Void
set_next
(value: BACKTRACKING_NODE_LIST)
effective procedure
{
ANY
}
top
ensure
definition:
next
= value
explore
(explorer:
BACKTRACKING
)
deferred procedure
{
ANY
}
top
That feature must update the state of 'explorer'.
fill_tagged_out_memory
effective procedure
{
ANY
}
top
Append a viewable information in
tagged_out_memory
in order to affect the behavior of
out
,
tagged_out
, etc.
require
locked:
tagged_out_locked
ensure
still_locked:
tagged_out_locked
fill_tagged_out_memory_flag
:
BOOLEAN
writable attribute
{}
top
do_fill_tagged_out_memory
deferred procedure
{}
top