Interface TreeKernel<T>

Type Parameters:
T - type of TreeKernel node labels
All Superinterfaces:
Iterable<T>, Standard<Tree<T>>
All Known Subinterfaces:
Tree<T>
All Known Implementing Classes:
Tree1, TreeSecondary

public interface TreeKernel<T> extends Standard<Tree<T>>, Iterable<T>
Tree kernel component with primary methods. (Note: by package-wide convention, all references are non-null.)
Mathematical Definitions:
PRE_ORDER(
  t: tree of T
 ): string of T satisfies
 if t = empty_tree
  then PRE_ORDER(tree) = <>
  else there exists root: T, children: string of tree of T
        (t = compose(root, children) and
         PRE_ORDER(t) = <root> * STRING_PRE_ORDER(children))

STRING_PRE_ORDER(
  s: string of tree of T
 ): string of T satisfies
 if s = empty_string
  then STRING_PRE_ORDER(s) = <>
  else there exists t: tree of T, rest: string of tree of T
        (s = <t> * rest and
         STRING_PRE_ORDER(s) = PRE_ORDER(t) * STRING_PRE_ORDER(rest))
Mathematical Model (abstract value and abstract invariant of this):
type TreeKernel is modeled by tree of T
Constructor(s) (initial abstract value(s) of this):
():
 ensures
  this = empty_tree
Iterator String (abstract value of ~this):
~this.seen * ~this.unseen = PRE_ORDER(this)
  • Method Summary

    Modifier and Type
    Method
    Description
    void
    assemble(T root, Sequence<Tree<T>> children)
    Assembles in this a tree with root label root and subtrees children; the declaration notwithstanding, the dynamic type of each entry of children must be the same as the dynamic type of this and the dynamic type of children must be the same as that returned by newSequenceOfTree.
    disassemble(Sequence<Tree<T>> children)
    Disassembles this into its root label, which is returned as the value of the function, and subtrees in children; the declaration notwithstanding, the dynamic type of children must be the same as that returned by newSequenceOfTree.
    Creates and returns an empty Sequence<Tree<T>> of the dynamic type needed in assemble and disassemble.
    int
    Reports the size of this.

    Methods inherited from interface java.lang.Iterable

    forEach, iterator, spliterator

    Methods inherited from interface components.standard.Standard

    clear, newInstance, transferFrom
  • Method Details

    • newSequenceOfTree

      Creates and returns an empty Sequence<Tree<T>> of the dynamic type needed in assemble and disassemble.
      Returns:
      a new empty Sequence<Tree<T>>
      Ensures:
      newSequenceOfTree = <>
    • assemble

      void assemble(T root, Sequence<Tree<T>> children)
      Assembles in this a tree with root label root and subtrees children; the declaration notwithstanding, the dynamic type of each entry of children must be the same as the dynamic type of this and the dynamic type of children must be the same as that returned by newSequenceOfTree.
      Parameters:
      root - the root label
      children - the subtrees
      Aliases:
      reference root
      Replaces:
      this
      Clears:
      children
      Ensures:
      this = compose(root, #children)
    • disassemble

      T disassemble(Sequence<Tree<T>> children)
      Disassembles this into its root label, which is returned as the value of the function, and subtrees in children; the declaration notwithstanding, the dynamic type of children must be the same as that returned by newSequenceOfTree.
      Parameters:
      children - the subtrees
      Returns:
      the root label
      Replaces:
      children
      Clears:
      this
      Requires:
      this /= empty_tree
      Ensures:
      #this = compose(disassemble, children)
    • size

      int size()
      Reports the size of this.
      Returns:
      the size
      Ensures:
      size = |this|