Learning Objectives

• Define binary trees recursively as a data structure.
• Implement a TreeNode class in Java with recursive methods.
• Prove properties of tree algorithms by structural induction (Module 6).
• Implement and analyze recursive traversals (preorder, inorder, postorder).
• Connect trees to expression evaluation (Module 6 Class 3) and recursion.

Concept Overview

Recursive Definition

A binary tree is either:

1. Empty (null), or
2. A node with a value, a left subtree, and a right subtree.

This is a recursively defined structure (Module 6 Class 3).

Terminology

Traversal Orders

Formal Notation

Worked Examples

Example 1: Size by Structural Induction

Claim: size(T) returns $|T|$.

public int size() {
    int ls = (left == null) ? 0 : left.size();
    int rs = (right == null) ? 0 : right.size();
    return 1 + ls + rs;
}

Proof by structural induction:

• Base: Empty tree (null): size returns 0. $|null| = 0$. ✓
• Inductive step: Assume left.size() = $|T.L|$ and right.size() = $|T.R|$. Then size() = $1 + |T.L| + |T.R| = |T|$. ✓ $\blacksquare$

Example 2: Height

public int height() {
    int lh = (left == null) ? -1 : left.height();
    int rh = (right == null) ? -1 : right.height();
    return 1 + Math.max(lh, rh);
}

Structural induction: Base: single node (both children null): $1 + \max(-1, -1) = 0$. ✓

Inductive: $h(T) = 1 + \max(h(T.L), h(T.R))$, matching the definition.

Example 3: Counting Leaves

public int countLeaves() {
    if (left == null && right == null) return 1;
    int ll = (left == null) ? 0 : left.countLeaves();
    int rl = (right == null) ? 0 : right.countLeaves();
    return ll + rl;
}

Example 4: Inorder Traversal

public void inorder(List<Integer> result) {
    if (left != null) left.inorder(result);
    result.add(value);
    if (right != null) right.inorder(result);
}

For a BST, inorder traversal produces sorted output.

Example 5: Expression Tree Evaluation (Module 6 Callback)

       *
      / \
     +   3
    / \
   2   5

Postorder: 2, 5, +, 3, * → $(2 + 5) \times 3 = 21$.

Proof Techniques Spotlight

Structural Induction on Trees

To prove property $P(T)$ for all binary trees $T$:

1. Base case: Prove $P(\text{null})$ (or $P(\text{leaf})$).
2. Inductive step: Assume $P(T.L)$ and $P(T.R)$. Prove $P(T)$.

This parallels recursion: the base case is the simplest tree; the inductive step combines results from subtrees.

Size-Height Relationship

Theorem: For any binary tree $T$ with $n$ nodes and height $h$:

• Left bound: a path of $h + 1$ nodes (degenerate tree).
• Right bound: a complete binary tree (all levels full).

Java Deep Dive

import java.util.*;

public class TreeNode {
    int value;
    TreeNode left;
    TreeNode right;

    public TreeNode(int value) {
        this.value = value;
    }

    public TreeNode(int value, TreeNode left, TreeNode right) {
        this.value = value;
        this.left = left;
        this.right = right;
    }

    // --- Size ---
    public int size() {
        int ls = (left == null) ? 0 : left.size();
        int rs = (right == null) ? 0 : right.size();
        return 1 + ls + rs;
    }

    // --- Height ---
    public int height() {
        int lh = (left == null) ? -1 : left.height();
        int rh = (right == null) ? -1 : right.height();
        return 1 + Math.max(lh, rh);
    }

    // --- Count Leaves ---
    public int countLeaves() {
        if (left == null && right == null) return 1;
        int ll = (left == null) ? 0 : left.countLeaves();
        int rl = (right == null) ? 0 : right.countLeaves();
        return ll + rl;
    }

    // --- Count Internal Nodes ---
    public int countInternal() {
        if (left == null && right == null) return 0;
        int li = (left == null) ? 0 : left.countInternal();
        int ri = (right == null) ? 0 : right.countInternal();
        return 1 + li + ri;
    }

    // --- Traversals ---
    public List<Integer> preorder() {
        List<Integer> result = new ArrayList<>();
        preorderHelper(result);
        return result;
    }
    private void preorderHelper(List<Integer> result) {
        result.add(value);
        if (left != null) left.preorderHelper(result);
        if (right != null) right.preorderHelper(result);
    }

    public List<Integer> inorder() {
        List<Integer> result = new ArrayList<>();
        inorderHelper(result);
        return result;
    }
    private void inorderHelper(List<Integer> result) {
        if (left != null) left.inorderHelper(result);
        result.add(value);
        if (right != null) right.inorderHelper(result);
    }

    public List<Integer> postorder() {
        List<Integer> result = new ArrayList<>();
        postorderHelper(result);
        return result;
    }
    private void postorderHelper(List<Integer> result) {
        if (left != null) left.postorderHelper(result);
        if (right != null) right.postorderHelper(result);
        result.add(value);
    }

    // --- Is Full Binary Tree ---
    public boolean isFull() {
        if (left == null && right == null) return true;
        if (left == null || right == null) return false;
        return left.isFull() && right.isFull();
    }

    // --- Mirror ---
    public TreeNode mirror() {
        TreeNode ml = (right == null) ? null : right.mirror();
        TreeNode mr = (left == null) ? null : left.mirror();
        return new TreeNode(value, ml, mr);
    }

    // --- Build full binary tree of given height ---
    public static TreeNode buildFull(int height) {
        if (height < 0) return null;
        if (height == 0) return new TreeNode(0);
        TreeNode left = buildFull(height - 1);
        TreeNode right = buildFull(height - 1);
        return new TreeNode(0, left, right);
    }

    // --- Pretty print ---
    public void print(String prefix, boolean isLeft) {
        if (right != null) right.print(prefix + (isLeft ? "│   " : "    "), false);
        System.out.println(prefix + (isLeft ? "└── " : "┌── ") + value);
        if (left != null) left.print(prefix + (isLeft ? "    " : "│   "), true);
    }

    // --- Demo ---
    public static void main(String[] args) {
        System.out.println("=== Binary Trees ===\n");

        // Build a sample tree:
        //        1
        //       / \
        //      2   3
        //     / \   \
        //    4   5   6
        TreeNode tree = new TreeNode(1,
                new TreeNode(2, new TreeNode(4), new TreeNode(5)),
                new TreeNode(3, null, new TreeNode(6)));

        tree.print("", false);

        System.out.println("\nSize: " + tree.size());           // 6
        System.out.println("Height: " + tree.height());         // 2
        System.out.println("Leaves: " + tree.countLeaves());    // 3
        System.out.println("Internal: " + tree.countInternal());// 3

        System.out.println("\nPreorder:  " + tree.preorder());  // [1,2,4,5,3,6]
        System.out.println("Inorder:   " + tree.inorder());    // [4,2,5,1,3,6]
        System.out.println("Postorder: " + tree.postorder());  // [4,5,2,6,3,1]

        System.out.println("\nIs full? " + tree.isFull());      // false

        // Full binary tree
        TreeNode full = buildFull(3);
        System.out.println("\nFull tree (height 3):");
        full.print("", false);
        System.out.println("Size: " + full.size());             // 15 = 2^4 - 1
        System.out.println("Leaves: " + full.countLeaves());    // 8 = 2^3
        System.out.println("Internal: " + full.countInternal());// 7
        System.out.println("L = I + 1? " + (full.countLeaves() == full.countInternal() + 1));

        // Mirror
        System.out.println("\nMirror:");
        tree.mirror().print("", false);
    }
}

Historical Context

Arthur Cayley (1857) was among the first to study tree structures mathematically, counting the number of labeled trees on $n$ vertices ($n^{n-2}$, Cayley's formula).

Binary trees became central in computer science through Donald Knuth's The Art of Computer Programming (1968), where he systematized traversal algorithms and their analysis.

Expression trees connect to Module 6's structural induction and recursion — evaluating an expression tree is one of the oldest examples of structural recursion in programming.

Slide-Ready Problem Sets

Slide Set A: Conceptual Questions

A1. Give the recursive definition of a binary tree.

A2. What are the three traversal orders? For each, state which visits the root first/second/last.

A3. What is the height of a tree with a single node? An empty tree?

A4. For a full binary tree of height 3, how many nodes, leaves, and internal nodes are there?

Slide Set B: Proof Problems

B1. Prove by structural induction: size(T) returns $|T|$.

B2. Prove: for a full binary tree, $L = I + 1$ (leaves = internal nodes + 1).

B3. Prove: $h + 1 \leq |T| \leq 2^{h+1} - 1$.

Slide Set C: Java Coding Problems

C1. Implement size(), height(), countLeaves() recursively.

C2. Implement all three traversals and verify on a sample tree.

C3. Implement buildFull(height) and verify $|T| = 2^{h+1} - 1$.

Full Problem Set

Discrete Math Problems

DM1. Define a binary tree recursively. State the base case and the recursive case.

DM2. Prove by structural induction: for every binary tree $T$, $|T| = L(T) + I(T)$.

DM3. Prove by structural induction: for a full binary tree, $L(T) = I(T) + 1$.

DM4. Prove: the number of null pointers in a binary tree with $n$ nodes is $n + 1$.

DM5. Prove: inorder traversal of a BST visits nodes in sorted order.

Java Programming Problems

JP1. Implement TreeNode with size, height, countLeaves, countInternal, and all three traversals.

JP2. Implement buildFull(height) and verify: size = $2^{h+1} - 1$, leaves = $2^h$, $L = I + 1$.

JP3. Implement mirror(TreeNode root) that returns a mirror image. Prove by structural induction that mirror(mirror(T)) == T.

JP4. Implement isBalanced(TreeNode root): a tree is balanced if for every node, the heights of left and right subtrees differ by at most 1.

JP5. Build a tree from preorder and inorder traversal lists. Verify by comparing the tree's traversals with the originals.

Bridge Problems

BR1. Module 6 Class 3 defined expressions recursively ($E ::= n \mid E + E \mid E \times E$). Show that expression trees are binary trees where leaves are numbers and internal nodes are operators.

BR2. Module 8: traversal algorithms have loop invariants (for iterative versions). State the invariant for an iterative inorder traversal using a stack.

Solutions

DM3 Solution: Full Binary Tree Theorem

Proof by structural induction on $T$.

Base: A single node (leaf). $L = 1$, $I = 0$. $L = I + 1 = 1$. ✓

Inductive step: Let $T$ have root with left subtree $T_L$ and right subtree $T_R$ (both non-empty, since $T$ is full).

By inductive hypothesis: $L(T_L) = I(T_L) + 1$ and $L(T_R) = I(T_R) + 1$.

DM4 Solution: Null Pointers

Each node has 2 pointers. Total pointers: $2n$. Each non-null pointer points to exactly one node (there are $n - 1$ such pointers, since every node except the root is pointed to by its parent). Null pointers: $2n - (n-1) = n + 1$. $\blacksquare$

Learning Objectives

• Prove the full binary tree theorem ($L = I + 1$) and total node count ($N = 2I + 1$).
• Define balanced binary trees and analyze their height bounds.
• Implement methods to check fullness and balance.
• Connect tree properties to complexity analysis ($O(\log n)$ vs $O(n)$).
• Apply structural induction and counting (Modules 6–7) to tree theorems.

Concept Overview

Full Binary Trees

A binary tree is full if every node has either 0 or 2 children. No node has exactly one child.

Fundamental properties of a full binary tree:

Complete Binary Trees

A binary tree is complete if every level except possibly the last is full, and the last level is filled from left to right.

For a complete binary tree of height $h$:

Balanced Binary Trees

A binary tree is balanced (height-balanced) if for every node, the heights of the left and right subtrees differ by at most 1:

Height Bounds

Key insight: Balancing a BST keeps height $O(\log n)$, ensuring efficient operations.

Formal Notation

Worked Examples

Example 1: Full Binary Tree Theorem ($L = I + 1$)

Proof by structural induction.

Base: Single node: $L = 1, I = 0, L = I + 1$. ✓

Inductive step: $T$ has root with children $T_L, T_R$ (both non-empty since $T$ is full).

By IH: $L(T_L) = I(T_L) + 1$ and $L(T_R) = I(T_R) + 1$.

Example 2: Total Nodes = $2I + 1$

Equivalently: $N = 2L - 1$.

Example 3: Height Bound for Balanced Trees

Claim: A balanced binary tree with $n$ nodes has height $h \leq 1.44 \log_2(n+1)$.

Sketch: Let $N(h)$ be the minimum number of nodes in a balanced tree of height $h$. Then:

This is similar to Fibonacci! In fact, $N(h) = F_{h+2} - 1$ where $F$ is the Fibonacci sequence. Since $F_k \approx \phi^k / \sqrt{5}$, we get $n \geq \phi^h / \sqrt{5}$, giving $h = O(\log_\phi n) = O(1.44 \log_2 n)$.

Example 4: Complete Binary Tree Node Count

A complete binary tree of height $h = 3$ has between $2^3 = 8$ and $2^4 - 1 = 15$ nodes.

A complete binary tree with $n = 10$ nodes has height $h = \lfloor \log_2 10 \rfloor = 3$.

Example 5: Verifying Properties Computationally

For a full tree of height 4:

• $N = 2^5 - 1 = 31$
• $L = 2^4 = 16$
• $I = 15$
• $L = I + 1$? $16 = 15 + 1$. ✓

Proof Techniques Spotlight

Structural Induction on Trees (Revisited)

For full binary trees, the induction is cleaner because every internal node has exactly two children. The inductive step always has two subtrees to work with.

Counting Nodes by Level

For a complete binary tree: level $k$ has $2^k$ nodes (for $0 \leq k < h$), and level $h$ has between 1 and $2^h$ nodes. Total:

This uses the geometric series from Module 6.

Java Deep Dive

import java.util.*;

public class TreeProperties {

    static class TreeNode {
        int value;
        TreeNode left, right;

        TreeNode(int v) { this.value = v; }
        TreeNode(int v, TreeNode l, TreeNode r) {
            this.value = v; this.left = l; this.right = r;
        }
    }

    // --- Size ---
    public static int size(TreeNode t) {
        if (t == null) return 0;
        return 1 + size(t.left) + size(t.right);
    }

    // --- Height ---
    public static int height(TreeNode t) {
        if (t == null) return -1;
        return 1 + Math.max(height(t.left), height(t.right));
    }

    // --- Count Leaves ---
    public static int countLeaves(TreeNode t) {
        if (t == null) return 0;
        if (t.left == null && t.right == null) return 1;
        return countLeaves(t.left) + countLeaves(t.right);
    }

    // --- Count Internal Nodes ---
    public static int countInternal(TreeNode t) {
        if (t == null) return 0;
        if (t.left == null && t.right == null) return 0;
        return 1 + countInternal(t.left) + countInternal(t.right);
    }

    // --- Is Full ---
    public static boolean isFull(TreeNode t) {
        if (t == null) return true; // empty tree is vacuously full
        if (t.left == null && t.right == null) return true;
        if (t.left == null || t.right == null) return false;
        return isFull(t.left) && isFull(t.right);
    }

    // --- Is Balanced ---
    public static boolean isBalanced(TreeNode t) {
        return balancedHeight(t) != -2;
    }

    // Returns height if balanced, -2 if not
    private static int balancedHeight(TreeNode t) {
        if (t == null) return -1;
        int lh = balancedHeight(t.left);
        if (lh == -2) return -2;
        int rh = balancedHeight(t.right);
        if (rh == -2) return -2;
        if (Math.abs(lh - rh) > 1) return -2;
        return 1 + Math.max(lh, rh);
    }

    // --- Is Complete ---
    public static boolean isComplete(TreeNode t) {
        if (t == null) return true;
        Queue<TreeNode> queue = new LinkedList<>();
        queue.add(t);
        boolean seenNull = false;
        while (!queue.isEmpty()) {
            TreeNode node = queue.poll();
            if (node == null) {
                seenNull = true;
            } else {
                if (seenNull) return false;
                queue.add(node.left);
                queue.add(node.right);
            }
        }
        return true;
    }

    // --- Build Full Tree ---
    public static TreeNode buildFull(int height) {
        if (height < 0) return null;
        if (height == 0) return new TreeNode(0);
        return new TreeNode(0, buildFull(height - 1), buildFull(height - 1));
    }

    // --- Build Balanced BST from Sorted Array ---
    public static TreeNode buildBalancedBST(int[] sorted, int lo, int hi) {
        if (lo > hi) return null;
        int mid = lo + (hi - lo) / 2;
        return new TreeNode(sorted[mid],
                buildBalancedBST(sorted, lo, mid - 1),
                buildBalancedBST(sorted, mid + 1, hi));
    }

    // --- Verify Full Binary Tree Theorem ---
    public static void verifyFullTreeTheorem(int maxHeight) {
        for (int h = 0; h <= maxHeight; h++) {
            TreeNode t = buildFull(h);
            int n = size(t);
            int l = countLeaves(t);
            int i = countInternal(t);
            assert l == i + 1 : "L != I+1 for h=" + h;
            assert n == 2 * i + 1 : "N != 2I+1 for h=" + h;
            assert n == (int) Math.pow(2, h + 1) - 1 : "N != 2^(h+1)-1";
            assert l == (int) Math.pow(2, h) : "L != 2^h";
            System.out.printf("h=%d: N=%d, L=%d, I=%d, L=I+1? %b, N=2I+1? %b%n",
                    h, n, l, i, l == i + 1, n == 2 * i + 1);
        }
    }

    // --- Demo ---
    public static void main(String[] args) {
        System.out.println("=== Tree Properties ===\n");

        // Full tree verification
        System.out.println("--- Full Binary Tree Theorem ---");
        verifyFullTreeTheorem(6);

        // Balanced BST
        System.out.println("\n--- Balanced BST ---");
        int[] sorted = {1, 3, 5, 7, 9, 11, 13, 15};
        TreeNode bst = buildBalancedBST(sorted, 0, sorted.length - 1);
        System.out.println("Size: " + size(bst));
        System.out.println("Height: " + height(bst));
        System.out.println("Balanced? " + isBalanced(bst));
        System.out.println("Full? " + isFull(bst));
        System.out.println("Complete? " + isComplete(bst));

        // Degenerate tree (linked list)
        System.out.println("\n--- Degenerate Tree ---");
        TreeNode degenerate = new TreeNode(1,
                new TreeNode(2, new TreeNode(3, new TreeNode(4), null), null), null);
        System.out.println("Size: " + size(degenerate));
        System.out.println("Height: " + height(degenerate));
        System.out.println("Balanced? " + isBalanced(degenerate));

        // Height vs size comparison
        System.out.println("\n--- Height Comparison ---");
        for (int h = 0; h <= 10; h++) {
            TreeNode full = buildFull(h);
            System.out.printf("Full tree h=%2d: n=%5d, balanced=%b%n",
                    h, size(full), isBalanced(full));
        }
    }
}

Historical Context

AVL trees (Adelson-Velsky and Landis, 1962) were the first self-balancing binary search trees. Their balance condition (height difference $\leq 1$) guarantees $O(\log n)$ operations.

Red-black trees (Rudolf Bayer, 1972; given this name by Guibas and Sedgewick, 1978) use a coloring scheme to maintain approximate balance, guaranteeing height $\leq 2 \log_2(n + 1)$.

The full binary tree theorem ($L = I + 1$) appears in virtually every data structures textbook and is a classic exercise in structural induction.

Slide-Ready Problem Sets

Slide Set A: Conceptual Questions

A1. Define full, complete, and balanced binary trees. Give an example of each.

A2. For a full binary tree with 15 nodes, how many leaves and internal nodes?

A3. What is the maximum and minimum height of a binary tree with 100 nodes?

A4. Why does height $O(\log n)$ matter for BST operations?

Slide Set B: Proof Problems

B1. Prove $L = I + 1$ for full binary trees by structural induction.

B2. Prove: a complete binary tree of height $h$ has between $2^h$ and $2^{h+1} - 1$ nodes.

B3. Prove: the minimum number of nodes in a balanced tree of height $h$ satisfies $N(h) = N(h-1) + N(h-2) + 1$.

Slide Set C: Java Coding Problems

C1. Implement isFull, isBalanced, isComplete for binary trees.

C2. Build a full binary tree of height $h$ and verify $N = 2^{h+1} - 1$.

C3. Build a balanced BST from a sorted array and verify $h = O(\log n)$.

Full Problem Set

Discrete Math Problems

DM1. Prove: in a full binary tree, $N = 2L - 1$.

DM2. Prove: a binary tree with $n$ nodes has $n + 1$ null pointers.

DM3. Prove: for a complete binary tree of height $h$, the number of nodes at level $k$ ($0 \leq k < h$) is exactly $2^k$.

DM4. Show: the minimum number of nodes in a balanced tree of height $h$ is $N(h) = F_{h+3} - 1$ (where $F$ is Fibonacci). Verify for $h = 0, ..., 5$.

DM5. Prove by induction: a full binary tree of height $h$ has exactly $2^h$ leaves.

Java Programming Problems

JP1. Implement all tree property methods: size, height, countLeaves, countInternal, isFull, isBalanced, isComplete.

JP2. Build full trees of heights 0–10 and verify all properties of the full binary tree theorem.

JP3. Build balanced BSTs from sorted arrays of sizes 1, 3, 7, 15, 31, 63, 127. Verify heights are optimal.

JP4. Create a degenerate (linked-list) tree with $n$ nodes. Compare its height with a balanced tree of the same size.

JP5. Implement buildMinBalanced(int h) that constructs a balanced tree with the minimum number of nodes for height $h$. Verify it matches $F_{h+3} - 1$.

Bridge Problems

BR1. Module 7: The number of binary trees with $n$ nodes is the $n$-th Catalan number $C_n = \frac{1}{n+1}\binom{2n}{n}$. Compute $C_n$ for $n = 0, ..., 10$ using your binomial function from Module 7.

BR2. Module 6: The proof of $L = I + 1$ uses structural induction, which you first learned in Module 6 Class 3. Compare the technique here with the expression tree proof from that class.

Solutions

DM1 Solution

$N = L + I$. By the full binary tree theorem, $L = I + 1$. So $N = (I + 1) + I = 2I + 1 = 2(L - 1) + 1 = 2L - 1$. $\blacksquare$

DM2 Solution

Each of the $n$ nodes has 2 pointers (left, right). Total pointers: $2n$. Each non-root node is pointed to by exactly one parent pointer. Parent pointers used: $n - 1$. Null pointers: $2n - (n - 1) = n + 1$. $\blacksquare$

DM5 Solution

Base: $h = 0$: a single node is a leaf. $L = 1 = 2^0$. ✓

Inductive step: Assume a full binary tree of height $h$ has $2^h$ leaves. A full tree of height $h + 1$ has a root whose left and right subtrees are full trees of height $\leq h$. In a full tree of height exactly $h + 1$, at least one subtree has height $h$. If both are full trees of height $h$, then $L = 2^h + 2^h = 2^{h+1}$. ✓ $\blacksquare$

(Note: more precisely, a "perfect" binary tree of height $h$ has all leaves at level $h$; a "full" tree only requires every node to have 0 or 2 children. For perfect trees, $L = 2^h$ exactly.)

Learning Objectives

• Implement and prove correctness of BST insert, search, and delete.
• Understand heap structure and prove the heap property is maintained by insert/extract.
• Connect tree height to Big-O complexity for core operations.
• Survey formal verification tools and their role in software engineering.
• Synthesize proof techniques from the entire course (Modules 1–9).

Concept Overview

Binary Search Trees (BST)

A BST is a binary tree where for every node $v$:

• All values in $v.\text{left}$ are less than $v.\text{value}$
• All values in $v.\text{right}$ are greater than $v.\text{value}$

Operations and worst-case time:

Heaps and Priority Queues

A min-heap is a complete binary tree where every node's value is $\leq$ its children's values:

Array representation: For node at index $i$ (0-based):

• Left child: $2i + 1$
• Right child: $2i + 2$
• Parent: $\lfloor(i - 1) / 2\rfloor$

Big-O Notation

Common complexity classes:

Formal Verification

Formal verification uses mathematical proof to guarantee software correctness — not just testing. Key approaches:

1. Model checking: Exhaustive state-space exploration (finite systems)
2. Theorem proving: Interactive/automated provers (Coq, Isabelle, Lean)
3. Static analysis: Automated approximation of program behavior
4. Design by Contract: Runtime assertions as lightweight verification (Module 3, 8)

Formal Notation

Worked Examples

Example 1: BST Insert Correctness

Claim: Inserting a value $x$ into a valid BST produces a valid BST.

Proof by structural induction on the BST.

Base: Empty tree → single node $x$ → valid BST. ✓

Inductive step: Let $T$ be a valid BST with root $r$.

• If $x < r$: by IH, inserting $x$ into $T_L$ produces a valid BST. The new $T_L$' contains only values $< r$ (since $T_L$ did, and $x < r$). So the full tree is a valid BST. ✓
• If $x > r$: symmetric argument on $T_R$. ✓
• If $x = r$: depends on policy (ignore, update, or allow duplicates).

$\blacksquare$

Example 2: Heap Insert (Bubble Up)

Claim: After inserting at the end of the array and bubbling up, the min-heap property is restored.

Proof outline:

1. Place new element at position $n$ (next available in complete tree).
2. While element is less than its parent, swap with parent.
3. Loop invariant: The heap property holds everywhere except possibly between the current node and its parent.
4. Termination: On each swap, the element moves to a lower index ($\lfloor(i-1)/2\rfloor < i$). Terminates at index 0.
5. At termination, either the element is $\geq$ its parent, or it's at the root. Either way, the heap property is fully restored.

$\blacksquare$

Example 3: Big-O Proof for BST Search

Claim: BST search is $O(h)$ where $h$ is the tree height.

Proof: Each comparison moves the search one level down. The tree has $h + 1$ levels. At most $h + 1$ comparisons are made. So search is $O(h)$.

For a balanced BST: $h = O(\log n)$, so search is $O(\log n)$.

For a degenerate BST: $h = n - 1$, so search is $O(n)$.

Example 4: Build-Heap is $O(n)$

The naive analysis gives $O(n \log n)$ (call siftDown $n/2$ times, each $O(\log n)$). But a tighter analysis uses the observation that most nodes are near the bottom:

This is an application of the sum formula techniques from Module 6.

Example 5: Formal Verification of reverseArray

Using Hoare logic (Module 8), we can verify array reversal:

Specification:

• Pre: $a$ is an array of length $n$, $a_0 = A$
• Post: $a[i] = A[n - 1 - i]$ for all $0 \leq i < n$

Loop invariant: At iteration $j$:

• $a[i] = A[n - 1 - i]$ for $0 \leq i < j$
• $a[n - 1 - i] = A[i]$ for $0 \leq i < j$
• $a[i] = A[i]$ for $j \leq i \leq n - 1 - j$

Variant: $\lfloor n/2 \rfloor - j$ (decreases each iteration, bounded below by 0).

Proof Techniques Spotlight

Course Proof Techniques Synthesis

Java Deep Dive

import java.util.*;

public class TreeApplications {

    // ========== BST ==========

    static class TreeNode {
        int value;
        TreeNode left, right;
        TreeNode(int v) { this.value = v; }
        TreeNode(int v, TreeNode l, TreeNode r) {
            this.value = v; this.left = l; this.right = r;
        }
    }

    // --- BST Search ---
    public static TreeNode bstSearch(TreeNode t, int key) {
        if (t == null) return null;
        if (key < t.value) return bstSearch(t.left, key);
        if (key > t.value) return bstSearch(t.right, key);
        return t;
    }

    // --- BST Insert ---
    public static TreeNode bstInsert(TreeNode t, int key) {
        if (t == null) return new TreeNode(key);
        if (key < t.value) t.left = bstInsert(t.left, key);
        else if (key > t.value) t.right = bstInsert(t.right, key);
        // key == t.value: no duplicates
        return t;
    }

    // --- BST Delete ---
    public static TreeNode bstDelete(TreeNode t, int key) {
        if (t == null) return null;
        if (key < t.value) {
            t.left = bstDelete(t.left, key);
        } else if (key > t.value) {
            t.right = bstDelete(t.right, key);
        } else {
            // Found node to delete
            if (t.left == null) return t.right;
            if (t.right == null) return t.left;
            // Two children: replace with in-order successor
            TreeNode successor = findMin(t.right);
            t.value = successor.value;
            t.right = bstDelete(t.right, successor.value);
        }
        return t;
    }

    public static TreeNode findMin(TreeNode t) {
        while (t.left != null) t = t.left;
        return t;
    }

    // --- BST Validity Check ---
    public static boolean isValidBST(TreeNode t) {
        return isValidBST(t, Integer.MIN_VALUE, Integer.MAX_VALUE);
    }

    private static boolean isValidBST(TreeNode t, int min, int max) {
        if (t == null) return true;
        if (t.value <= min || t.value >= max) return false;
        return isValidBST(t.left, min, t.value)
            && isValidBST(t.right, t.value, max);
    }

    // --- In-Order Traversal (should be sorted for BST) ---
    public static List<Integer> inOrder(TreeNode t) {
        List<Integer> result = new ArrayList<>();
        inOrderHelper(t, result);
        return result;
    }

    private static void inOrderHelper(TreeNode t, List<Integer> result) {
        if (t == null) return;
        inOrderHelper(t.left, result);
        result.add(t.value);
        inOrderHelper(t.right, result);
    }

    // --- Height ---
    public static int height(TreeNode t) {
        if (t == null) return -1;
        return 1 + Math.max(height(t.left), height(t.right));
    }

    // ========== MIN-HEAP ==========

    static class MinHeap {
        private int[] data;
        private int size;

        public MinHeap(int capacity) {
            data = new int[capacity];
            size = 0;
        }

        public int size() { return size; }

        public int peek() {
            if (size == 0) throw new NoSuchElementException("Heap is empty");
            return data[0];
        }

        public void insert(int value) {
            if (size == data.length) {
                data = Arrays.copyOf(data, data.length * 2);
            }
            data[size] = value;
            bubbleUp(size);
            size++;
            assert checkHeapInvariant() : "Heap invariant violated after insert";
        }

        public int extractMin() {
            if (size == 0) throw new NoSuchElementException("Heap is empty");
            int min = data[0];
            size--;
            data[0] = data[size];
            siftDown(0);
            assert checkHeapInvariant() : "Heap invariant violated after extractMin";
            return min;
        }

        private void bubbleUp(int i) {
            // Invariant: heap property holds everywhere except
            // possibly between data[i] and data[parent(i)]
            while (i > 0 && data[i] < data[parent(i)]) {
                swap(i, parent(i));
                i = parent(i);
            }
            // Post: heap property fully restored
        }

        private void siftDown(int i) {
            // Variant: distance from i to bottom level (decreases each step)
            while (leftChild(i) < size) {
                int smallest = i;
                int left = leftChild(i);
                int right = rightChild(i);
                if (left < size && data[left] < data[smallest]) smallest = left;
                if (right < size && data[right] < data[smallest]) smallest = right;
                if (smallest == i) break;
                swap(i, smallest);
                i = smallest;
            }
        }

        private int parent(int i) { return (i - 1) / 2; }
        private int leftChild(int i) { return 2 * i + 1; }
        private int rightChild(int i) { return 2 * i + 2; }

        private void swap(int i, int j) {
            int tmp = data[i]; data[i] = data[j]; data[j] = tmp;
        }

        // Verify heap invariant
        public boolean checkHeapInvariant() {
            for (int i = 1; i < size; i++) {
                if (data[i] < data[parent(i)]) return false;
            }
            return true;
        }

        @Override
        public String toString() {
            return Arrays.toString(Arrays.copyOf(data, size));
        }
    }

    // ========== BIG-O COMPLEXITY MEASUREMENT ==========

    public static void measureBSTComplexity() {
        System.out.println("--- BST Operation Timing ---\n");
        int[] sizes = {1000, 10000, 100000};
        Random rng = new Random(42);

        for (int n : sizes) {
            // Balanced BST (from sorted array)
            int[] sorted = new int[n];
            for (int i = 0; i < n; i++) sorted[i] = i;
            TreeNode balanced = buildBalanced(sorted, 0, n - 1);

            // Degenerate BST (insert in order)
            TreeNode degenerate = null;
            int degN = Math.min(n, 10000); // cap to avoid stack overflow
            for (int i = 0; i < degN; i++) {
                degenerate = bstInsert(degenerate, i);
            }

            // Search timing
            long start = System.nanoTime();
            for (int i = 0; i < 1000; i++) {
                bstSearch(balanced, rng.nextInt(n));
            }
            long balancedTime = System.nanoTime() - start;

            System.out.printf("n=%6d | Balanced BST h=%d, 1000 searches: %,d ns%n",
                    n, height(balanced), balancedTime);
        }
    }

    private static TreeNode buildBalanced(int[] sorted, int lo, int hi) {
        if (lo > hi) return null;
        int mid = lo + (hi - lo) / 2;
        return new TreeNode(sorted[mid],
                buildBalanced(sorted, lo, mid - 1),
                buildBalanced(sorted, mid + 1, hi));
    }

    // ========== FORMAL VERIFICATION DEMO ==========

    // Verified reverseArray with loop invariant and variant
    public static void reverseArray(int[] a) {
        int n = a.length;
        // Pre: a is a valid array
        int[] original = Arrays.copyOf(a, n); // ghost variable for verification
        for (int j = 0; j < n / 2; j++) {
            // Invariant: a[i] = original[n-1-i] for 0 <= i < j
            //            a[n-1-i] = original[i] for 0 <= i < j
            //            a[i] = original[i] for j <= i <= n-1-j
            // Variant: n/2 - j
            int tmp = a[j];
            a[j] = a[n - 1 - j];
            a[n - 1 - j] = tmp;
            // Check invariant
            for (int i = 0; i <= j; i++) {
                assert a[i] == original[n - 1 - i] : "Invariant violated at i=" + i;
                assert a[n - 1 - i] == original[i] : "Invariant violated (mirror)";
            }
        }
        // Post: a[i] = original[n-1-i] for all i
        for (int i = 0; i < n; i++) {
            assert a[i] == original[n - 1 - i] : "Postcondition violated";
        }
    }

    // ========== DEMO ==========

    public static void main(String[] args) {
        System.out.println("=== Trees, Complexity and Verification ===\n");

        // BST Demo
        System.out.println("--- BST Operations ---");
        TreeNode bst = null;
        int[] keys = {50, 30, 70, 20, 40, 60, 80};
        for (int k : keys) bst = bstInsert(bst, k);
        System.out.println("In-order: " + inOrder(bst));
        System.out.println("Valid BST? " + isValidBST(bst));
        System.out.println("Height: " + height(bst));

        System.out.println("Search 40: " + (bstSearch(bst, 40) != null));
        System.out.println("Search 99: " + (bstSearch(bst, 99) != null));

        bst = bstDelete(bst, 30);
        System.out.println("After delete 30: " + inOrder(bst));
        System.out.println("Still valid BST? " + isValidBST(bst));

        // Min-Heap Demo
        System.out.println("\n--- Min-Heap ---");
        MinHeap heap = new MinHeap(16);
        int[] vals = {42, 17, 8, 31, 5, 23, 12, 3};
        for (int v : vals) {
            heap.insert(v);
            System.out.println("  Inserted " + v + ": " + heap);
        }
        System.out.println("Extracting in order:");
        while (heap.size() > 0) {
            System.out.println("  " + heap.extractMin());
        }

        // Big-O Measurement
        System.out.println("\n--- Complexity Measurement ---");
        measureBSTComplexity();

        // Verified Reverse
        System.out.println("\n--- Verified reverseArray ---");
        int[] arr = {1, 2, 3, 4, 5, 6, 7, 8};
        System.out.println("Before: " + Arrays.toString(arr));
        reverseArray(arr);
        System.out.println("After:  " + Arrays.toString(arr));

        // Formal Verification Survey
        System.out.println("\n--- Formal Verification Tools ---");
        System.out.println("Tool          | Type             | Language");
        System.out.println("Coq           | Theorem prover   | Gallina");
        System.out.println("Isabelle/HOL  | Theorem prover   | Isar");
        System.out.println("Lean          | Theorem prover   | Lean");
        System.out.println("Dafny         | Auto verifier    | Dafny");
        System.out.println("SPARK/Ada     | Design by Contract| Ada subset");
        System.out.println("JML           | Spec language    | Java");
        System.out.println("TLA+          | Model checker    | TLA+");
        System.out.println("\nIn this course, we used a lightweight form of");
        System.out.println("verification: Hoare logic + assertions in Java.");
    }
}

Historical Context

Binary search trees date to the late 1950s (Conway and Berners-Lee, 1959). The problem of balancing them has driven decades of innovation: AVL trees (1962), red-black trees (1978), splay trees (1985), and treaps (1989).

Heaps were introduced by J.W.J. Williams in 1964 alongside heapsort. The elegant array representation and the $O(n)$ build-heap algorithm make them a textbook favorite.

Big-O notation was introduced by Paul Bachmann (1894) and made standard by Edmund Landau. Donald Knuth popularized it in computer science.

Formal verification has a rich history: Floyd-Hoare logic (1969), Dijkstra's weakest precondition calculus (1975), and modern provers like Coq (used to verify the C compiler CompCert) and seL4 (a verified OS microkernel).

Slide-Ready Problem Sets

Slide Set A: Conceptual Questions

A1. What is the BST invariant? Why does in-order traversal produce sorted output?

A2. Describe the difference between a BST and a heap. Can a heap be used for sorted output?

A3. Explain why balanced BST search is $O(\log n)$ while degenerate BST search is $O(n)$.

A4. What does formal verification guarantee that testing cannot?

Slide Set B: Proof Problems

B1. Prove BST insert preserves the BST invariant by structural induction.

B2. Prove heap bubble-up terminates and restores the heap property.

B3. Prove: $f(n) = 3n^2 + 5n + 7$ is $O(n^2)$. Find explicit $c$ and $n_0$.

B4. State the loop invariant for BST search. Prove correctness.

Slide Set C: Java Coding Problems

C1. Implement BST insert, search, and delete. Verify with in-order traversal.

C2. Implement a min-heap with insert and extractMin. Verify the heap invariant with assertions.

C3. Time BST search for balanced vs degenerate trees of increasing size. Plot or display the results.

Full Problem Set

Discrete Math Problems

DM1. Prove that in-order traversal of a valid BST produces values in ascending order (by structural induction).

DM2. Prove: $5n^3 + 2n^2 + n = O(n^3)$. Exhibit $c$ and $n_0$.

DM3. Prove: bubble-up in a min-heap terminates (state the variant function) and restores the heap invariant (state and verify the loop invariant).

DM4. Prove: build-heap is $O(n)$, not $O(n \log n)$. Use the sum $\sum_{k=0}^{h} k \cdot 2^{h-k}$.

DM5. Prove: BST delete preserves the BST invariant (consider all three cases: leaf, one child, two children).

DM6. Starting from the Hoare triple framework (Module 8), write the full specification for bstSearch(t, key) including precondition, postcondition, and loop/recursion variant.

Java Programming Problems

JP1. Implement a complete BST with insert, search, delete, findMin, findMax, inOrder. Verify that in-order output is always sorted.

JP2. Implement a min-heap with invariant checking. Show it can function as a priority queue.

JP3. Implement heapsort using your min-heap. Prove a sorting invariant.

JP4. Measure and compare search times for balanced BST, degenerate BST, and Arrays.binarySearch on the same sorted data.

JP5. Implement a verified reverseArray with assertions checking the loop invariant and postcondition. Run with -ea to enable assertions.

Bridge Problems

BR1. Module 8 + 9: Write the complete Hoare-logic correctness proof for heapInsert: precondition, loop invariant, variant, postcondition.

BR2. Modules 6–9 Synthesis: The number of structurally distinct BSTs with $n$ keys is the $n$-th Catalan number (Module 7 bridge). Use structural induction (Module 6) to prove the recurrence $C_n = \sum_{i=0}^{n-1} C_i \cdot C_{n-1-i}$. Then implement it in Java and verify against the closed form $C_n = \frac{1}{n+1}\binom{2n}{n}$.

BR3. Reflection: Write a one-page essay on the role of formal verification in software engineering. How do the proof techniques from this course (direct proof, induction, loop invariants, specifications) form a foundation for tools like Coq or Dafny?

Solutions

DM1 Solution

Claim: In-order traversal of a valid BST produces values in ascending order.

Proof by structural induction.

Base: Empty tree produces empty list. ✓ Single node produces [v]. ✓

Inductive step: BST $T$ with root $r$, left subtree $T_L$, right subtree $T_R$. By BST invariant: all values in $T_L < r < $ all values in $T_R$.

By IH: inOrder($T_L$) is ascending and inOrder($T_R$) is ascending.

inOrder($T$) = inOrder($T_L$) ++ [$r$] ++ inOrder($T_R$).

• inOrder($T_L$) is ascending (by IH).
• Last element of inOrder($T_L$) $< r$ (by BST invariant).
• $r <$ first element of inOrder($T_R$) (by BST invariant).
• inOrder($T_R$) is ascending (by IH).

Therefore inOrder($T$) is ascending. $\blacksquare$

DM2 Solution

We need $c, n_0$ such that $5n^3 + 2n^2 + n \leq cn^3$ for all $n \geq n_0$.

For $n \geq 1$: $n \leq n^3$ and $n^2 \leq n^3$. So $5n^3 + 2n^2 + n \leq 5n^3 + 2n^3 + n^3 = 8n^3$.

Choose $c = 8, n_0 = 1$. $\blacksquare$

JP2 Solution Sketch

MinHeap pq = new MinHeap(16);
// Priority queue usage: process tasks by priority
pq.insert(5);  // low priority task
pq.insert(1);  // highest priority
pq.insert(3);
while (pq.size() > 0) {
    System.out.println("Processing priority: " + pq.extractMin());
}
// Output: 1, 3, 5  (ascending order = highest priority first)