001package components.tree;
002
003import components.sequence.Sequence;
004import components.standard.Standard;
005
006/**
007 * Tree kernel component with primary methods. (Note: by package-wide
008 * convention, all references are non-null.)
009 *
010 * @param <T>
011 *            type of {@code TreeKernel} node labels
012 * @mathdefinitions {@code
013 * PRE_ORDER(
014 *   t: tree of T
015 *  ): string of T satisfies
016 *  if t = empty_tree
017 *   then PRE_ORDER(tree) = <>
018 *   else there exists root: T, children: string of tree of T
019 *         (t = compose(root, children) and
020 *          PRE_ORDER(t) = <root> * STRING_PRE_ORDER(children))
021 *
022 * STRING_PRE_ORDER(
023 *   s: string of tree of T
024 *  ): string of T satisfies
025 *  if s = empty_string
026 *   then STRING_PRE_ORDER(s) = <>
027 *   else there exists t: tree of T, rest: string of tree of T
028 *         (s = <t> * rest and
029 *          STRING_PRE_ORDER(s) = PRE_ORDER(t) * STRING_PRE_ORDER(rest))
030 * }
031 * @mathmodel type TreeKernel is modeled by tree of T
032 * @initially <pre>
033 * ():
034 *  ensures
035 *   this = empty_tree
036 * </pre>
037 * @iterator ~this.seen * ~this.unseen = PRE_ORDER(this)
038 */
039public interface TreeKernel<T> extends Standard<Tree<T>>, Iterable<T> {
040
041    /**
042     * Creates and returns an empty {@code Sequence<Tree<T>>} of the dynamic
043     * type needed in {@code assemble} and {@code disassemble}.
044     *
045     * @return a new empty {@code Sequence<Tree<T>>}
046     * @ensures {@code newSequenceOfTree = <>}
047     */
048    Sequence<Tree<T>> newSequenceOfTree();
049
050    /**
051     * Assembles in {@code this} a tree with root label {@code root} and
052     * subtrees {@code children}; the declaration notwithstanding, the
053     * <i>dynamic</i> type of each entry of {@code children} must be the same as
054     * the <i>dynamic</i> type of {@code this} and the <i>dynamic</i> type of
055     * {@code children} must be the same as that returned by
056     * {@code newSequenceOfTree}.
057     *
058     * @param root
059     *            the root label
060     * @param children
061     *            the subtrees
062     * @aliases reference {@code root}
063     * @replaces this
064     * @clears children
065     * @ensures this = compose(root, #children)
066     */
067    void assemble(T root, Sequence<Tree<T>> children);
068
069    /**
070     * Disassembles {@code this} into its root label, which is returned as the
071     * value of the function, and subtrees in {@code children}; the declaration
072     * notwithstanding, the <i>dynamic</i> type of {@code children} must be the
073     * same as that returned by {@code newSequenceOfTree}.
074     *
075     * @param children
076     *            the subtrees
077     * @return the root label
078     * @replaces children
079     * @clears this
080     * @requires this /= empty_tree
081     * @ensures #this = compose(disassemble, children)
082     */
083    T disassemble(Sequence<Tree<T>> children);
084
085    /**
086     * Reports the size of {@code this}.
087     *
088     * @return the size
089     * @ensures size = |this|
090     */
091    int size();
092
093}