001package components.tree;
002
003/**
004 * {@code TreeKernel} enhanced with secondary methods.
005 *
006 * @param <T>
007 *            type of {@code Tree} labels
008 * @mathdefinitions {@code
009 * HEIGHT(
010 *   t: tree of T
011 *  ): integer satisfies
012 *  if t = empty_tree
013 *   then HEIGHT(t) = 0
014 *   else there exists root: T, children: string of tree of T
015 *         (t = compose(root, children) and
016 *          HEIGHT(t) = 1 + MAX_HEIGHT(children))
017 *
018 * MAX_HEIGHT(
019 *   s: string of tree of T
020 *  ): integer satisfies
021 *  if s = empty_string
022 *   then MAX_HEIGHT(s) = 0
023 *   else there exists t: tree of T, rest: string of tree of T
024 *         (s = <t> * rest and
025 *          MAX_HEIGHT(s) = max(HEIGHT(t), MAX_HEIGHT(rest))
026 * }
027 */
028public interface Tree<T> extends TreeKernel<T> {
029
030    /**
031     * Reports the root of {@code this}.
032     *
033     * @return the root entry of {@code this}
034     * @aliases reference returned by {@code root}
035     * @requires this /= empty_tree
036     * @ensures <pre>
037     * there exists children: string of tree of T
038     *     (this = compose(root, children))
039     * </pre>
040     */
041    T root();
042
043    /**
044     * Replaces the root of {@code this} with {@code x}, and returns the old
045     * root.
046     *
047     * @param x
048     *            the new root
049     * @return the old root
050     * @aliases reference {@code x}
051     * @updates this
052     * @requires this /= empty_tree
053     * @ensures <pre>
054     * there exists children: string of tree of T
055     *     (#this = compose(replaceRoot, children)  and
056     *      this = compose(x, children))
057     * </pre>
058     */
059    T replaceRoot(T x);
060
061    /**
062     * Reports the height of {@code this}.
063     *
064     * @return the height
065     * @ensures height = HEIGHT(this)
066     */
067    int height();
068
069    /**
070     * Adds the tree {@code st} at position {@code pos} in {@code this}; the
071     * declaration notwithstanding, the <i>dynamic</i> type of {@code st} must
072     * be the same as the <i>dynamic</i> type of {@code this}.
073     *
074     * @param pos
075     *            the position at which to add {@code st}
076     * @param st
077     *            the {@code Tree} to add
078     * @updates this
079     * @clears st
080     * @requires {@code
081     * this /= empty_tree  and
082     * 0 <= pos <= [number of children of this]
083     * }
084     * @ensures this = [#this with subtree #st inserted at position pos]
085     */
086    void addSubtree(int pos, Tree<T> st);
087
088    /**
089     * Removes and returns the subtree at position {@code pos} in {@code this}.
090     *
091     * @param pos
092     *            the position of the subtree to remove
093     * @return the subtree at position pos in {@code this}
094     * @updates this
095     * @requires {@code
096     * this /= empty_tree  and
097     * 0 <= pos < [number of children of this]
098     * }
099     * @ensures <pre>
100     * this =
101     *  [#this with subtree at position pos removed and returned as result]
102     * </pre>
103     */
104    Tree<T> removeSubtree(int pos);
105
106    /**
107     * Returns the number of subtrees of the root of {@code this}.
108     *
109     * @return the number of subtrees of the root of {@code this}
110     * @requires this /= empty_tree
111     * @ensures <pre>
112     * there exists root: T, children: string of tree of T
113     *     (this = compose(root, children)  and
114     *      numberOfSubtrees = |children|)
115     * </pre>
116     */
117    int numberOfSubtrees();
118
119}