+
Point of view
All features
deferred class BACKTRACKING_NODE_UNARY
Summary
top
node that reference one subnode
Direct parents
Inherit list: BACKTRACKING_NODE
Insert list: BACKTRACKING_NODE_FILL
Known children
Inherit list: BACKTRACKING_NODE_NOT, BACKTRACKING_NODE_OR_TRUE, BACKTRACKING_NODE_TRUE_OR, BACKTRACKING_NODE_UNDER_CUT_POINT
Class invariant
top
Overview
top
Features
{ANY}
{ANY}
{ANY}
{}
writable attribute
{ANY}
top
the node
make (value: BACKTRACKING_NODE)
effective procedure
{ANY}
top
require
  • value_not_void: value /= Void
ensure
  • definition: node = value
  • 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
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