class BACKTRACKING_NODE_TRUE_OR

Features exported to ANY

Alternative between nothing (as true) first and then a node

Direct parents

conformant parents

BACKTRACKING_NODE_UNARY

non-conformant parents

BACKTRACKING_NODE_GLOBALS

Summary

creation features

exported features

and/or basics

Details

explore (explorer: BACKTRACKING)

That feature must update the state of 'explorer'.

node: BACKTRACKING_NODE

the node

make (value: BACKTRACKING_NODE)

require

  • value_not_void: value /= Void

ensure

  • definition: node = value
  • 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

the_cut_node: BACKTRACKING_NODE_CUT
the_true_node: BACKTRACKING_NODE_TRUE
the_false_node: BACKTRACKING_NODE_FALSE
the_cut_and_false_node: BACKTRACKING_NODE_CUT_AND_FALSE

Class invariant