class BACKTRACKING_NODE_AND_PAIR

All features

Node for a sequence of 2 nodes

Direct parents

conformant parents

BACKTRACKING_NODE_BINARY

Summary

creation features

exported features

Details

explore (explorer: BACKTRACKING)

That feature must update the state of 'explorer'.

first: BACKTRACKING_NODE

first node of the sequence

second: BACKTRACKING_NODE

second node of the sequence

make (frst: BACKTRACKING_NODE, scnd: BACKTRACKING_NODE)

require

  • first_not_void: frst /= Void
  • second_not_void: scnd /= Void

ensure

  • definition: first = frst and second = scnd
  • first_not_void: first /= Void
  • second_not_void: second /= Void

set_first (value: BACKTRACKING_NODE)

require

  • value_not_void: value /= Void

ensure

  • definition: first = value
  • first_not_void: first /= Void

set_second (value: BACKTRACKING_NODE)

require

  • value_not_void: value /= Void

ensure

  • definition: second = value
  • second_not_void: second /= Void

Class invariant