class BACKTRACKING_NODE_AND_LIST

All features

Node for a sequence of list of nodes

Direct parents

conformant parents

BACKTRACKING_NODE_LIST

Summary

creation features

exported features

Details

explore (explorer: BACKTRACKING)

That feature must update the state of 'explorer'.

node: BACKTRACKING_NODE

first node of the list

next: BACKTRACKING_NODE_AND_LIST

remaining of the list

make (nod: BACKTRACKING_NODE, nxt: BACKTRACKING_NODE_AND_LIST)

require

  • value_not_void: nod /= Void

ensure

  • definition: node = nod and next = nxt
  • node_not_void: node /= Void

set_node (value: BACKTRACKING_NODE)

require

  • value_not_void: value /= Void

ensure

  • definition: node = value
  • node_not_void: node /= Void

set_next (value: BACKTRACKING_NODE_AND_LIST)

ensure

  • definition: next = value

Class invariant