+
Point of view
All features
class BACKTRACKING_NODE_AND_PAIR
Summary
Node for a sequence of 2 nodes
Direct parents
Inherit list: BACKTRACKING_NODE_BINARY
Class invariant
Overview
Creation features
Features
{ANY}
{}
{ANY}
{ANY}
{}
explore (explorer: BACKTRACKING)
effective procedure
{ANY}
That feature must update the state of 'explorer'.
do_fill_tagged_out_memory
effective procedure
{}
writable attribute
{ANY}
first node of the sequence
writable attribute
{ANY}
second node of the sequence
effective procedure
{ANY}
require
  • first_not_void: frst /= Void
  • second_not_void: scnd /= Void
ensure
set_first (value: BACKTRACKING_NODE)
effective procedure
{ANY}
require
  • value_not_void: value /= Void
ensure
  • definition: first = value
  • first_not_void: first /= Void
set_second (value: BACKTRACKING_NODE)
effective procedure
{ANY}
require
  • value_not_void: value /= Void
ensure
fill_tagged_out_memory
effective procedure
{ANY}
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
{}