001package components.binarytree;
002
003import components.standard.Standard;
004
005/**
006 * Binary tree kernel component with primary methods. (Note: by package-wide
007 * convention, all references are non-null.)
008 *
009 * @param <T>
010 *            type of {@code BinaryTreeKernel} node labels
011 * @mathdefinitions {@code
012 * IN_ORDER(
013 *   tree: binary tree of T
014 *  ): string of T satisfies
015 *  if tree = empty_tree
016 *   then IN_ORDER(tree) = <>
017 *   else there exists root: T, left, right: binary tree of T
018 *         (tree = compose(root, left, right) and
019 *          IN_ORDER(tree) = IN_ORDER(left) * <root> * IN_ORDER(right))
020 * }
021 * @mathmodel type BinaryTreeKernel is modeled by binary tree of T
022 * @initially <pre>
023 * ():
024 *  ensures
025 *   this = empty_tree
026 * </pre>
027 * @iterator ~this.seen * ~this.unseen = IN_ORDER(this)
028 */
029public interface BinaryTreeKernel<T> extends Standard<BinaryTree<T>>, Iterable<T> {
030
031    /**
032     * Assembles in {@code this} a tree with root label {@code root} and
033     * subtrees {@code left} and {@code right}; the declaration notwithstanding,
034     * the <i>dynamic</i> type of {@code left} and {@code right} must be the
035     * same as the <i>dynamic</i> type of {@code this}.
036     *
037     * @param root
038     *            the root label
039     * @param left
040     *            the left subtree
041     * @param right
042     *            the right subtree
043     * @aliases reference {@code root}
044     * @replaces this
045     * @clears left, right
046     * @ensures this = compose(root, #left, #right)
047     */
048    void assemble(T root, BinaryTree<T> left, BinaryTree<T> right);
049
050    /**
051     * Disassembles {@code this} into its root label, which is returned as the
052     * value of the function, and subtrees {@code left} and {@code right}; the
053     * declaration notwithstanding, the <i>dynamic</i> type of {@code left} and
054     * {@code right} must be the same as the <i>dynamic</i> type of {@code this}
055     * .
056     *
057     * @param left
058     *            the left subtree
059     * @param right
060     *            the right subtree
061     * @return the root label
062     * @replaces left, right
063     * @clears this
064     * @requires this /= empty_tree
065     * @ensures #this = compose(disassemble, left, right)
066     */
067    T disassemble(BinaryTree<T> left, BinaryTree<T> right);
068
069    /**
070     * Reports the size of {@code this}.
071     *
072     * @return the size
073     * @ensures size = |this|
074     */
075    int size();
076
077}