Formal Complexity Model
========================

.. contents:: :local:

Definitions
-----------

Let G = (V, E) be a directed graph with |V| = n vertices and |E| = m edges.

A **CWE-407 graph traversal defect** occurs when a function f satisfies all of the following:

1. f is called inside a loop that iterates O(n) times (one call per vertex or edge)
2. f accepts a collection L as an argument (or closes over L)
3. f performs a membership test ``x ∈ L`` where ``x`` is a graph node or edge identifier
4. L is represented as a list/array/vector such that ``x ∈ L`` costs O(|L|)
5. |L| grows with the traversal: |L| = O(n) at the point of the i-th call

Under these conditions, the total cost of all membership tests is:

.. math::

   \sum_{i=0}^{n-1} O(i) = O\!\left(\frac{n(n-1)}{2}\right) = O(n^2)

where the defective code achieves O(n²) and the achievable lower bound is O(n).

The Quadratic Proof
--------------------

**Theorem:** Any DFS or BFS graph traversal algorithm that maintains ``visited`` or ``onStack``
state as a list and performs a linear scan for membership has worst-case time complexity O(V²).

**Proof:**

Consider a Tarjan SCC traversal on a graph G = (V, E). The algorithm visits each vertex once.
For each vertex v visited, it performs one membership test on the ``stack`` structure:

- At the time of the i-th test, the stack contains at most i−1 elements
- The membership test on a list costs O(i)
- Summing over all vertices: T(n) = Σᵢ₌₁ⁿ O(i) = O(n(n+1)/2) = O(n²)

This result is tight: the ``starWithBackEdges(n)`` topology (one hub connected to n spokes,
each spoke with a back-edge to the hub) achieves exactly n(n+1)/2 − 1 comparisons in the
defective implementation. This is confirmed by unit test operation counts in
``tests/unit/GraphUtilsDefectTest.java``. ∎

The O(1) Membership Bound
--------------------------

**Theorem:** Hash table membership tests are O(1) amortized.

**Proof sketch:** A hash table with load factor α < 1 stores n elements in a table of size
⌈n/α⌉. Under a uniform hash function, the expected number of comparisons for a membership
test (with chaining) is:

.. math::

   E[\text{comparisons}] = 1 + \frac{\alpha}{2} = O(1)

as α is bounded by a constant (typically 0.75). Rehashing occurs at most O(log n) times
over n insertions, each rehash costs O(n), giving amortized O(1) per insertion. Since
membership tests do not trigger rehashing, they are O(1) worst-case after construction. ∎

For the specific use case of CWE-407 graph traversal fixes, the load factor argument is
conservative: the visited set is used write-heavy (one insert per vertex, one read per edge),
and the hash keys are object references or integer node IDs — both hash in O(1) time with no
collision risk from adversarial inputs, since the key space is controlled by the traversal.

Canonical Fix Complexity
-------------------------

After replacing the list with a hash set for visited/onStack state:

- DFS traversal: each vertex visited once, O(1) membership test per vertex → **O(V)**
- BFS traversal: each vertex enqueued once, O(1) set-membership check → **O(V + E)**
- Tarjan SCC: each vertex pushed/popped once, O(1) onStack test → **O(V + E)**
- Cycle detection: one O(1) set-insert per vertex → **O(V)**

All patched implementations achieve the theoretically optimal O(V + E) for connected-graph
traversal.

Exact Operation Counts (Measured)
-----------------------------------

The following operation counts are from unit tests that instrument comparison/insertion
counters directly (not wall-clock timing), verifying the formulas precisely:

.. list-table::
   :header-rows: 1
   :widths: 15 20 30 20 20

   * - Defect
     - V / N
     - Defective formula
     - Fixed formula
     - Formula name
   * - javac-0001
     - V nodes
     - V*(V+1)/2 - 1
     - V - 1
     - ``starWithBackEdges(V)``
   * - javac-0002a
     - N type vars
     - N*(N+1)/2
     - N
     - ``queryAll(N)``
   * - javac-0002b
     - V nodes, K calls
     - K*V
     - V + (K-1)
     - ``closureFixed K on chain(V)``
   * - javac-0003
     - V modules
     - V*(V-1)/2
     - V
     - ``linearChain(V)``
   * - javac-0004
     - M deps
     - M*(M-1)/2
     - M
     - ``addUnique(M)``
   * - javac-0005
     - B bounds
     - B*(B+1)
     - B
     - ``isEquiv forward vs reversed(B)``

The formulas are exact, not asymptotic. The unit tests verify equality, not inequality, at
each sample point.

Balanced BST vs Hash Table
---------------------------

Several fix patterns use balanced BST sets (``Data.Set`` in Haskell, ``gb_sets`` in Erlang,
``TreeSet`` in Java) rather than hash sets. These give O(log n) membership rather than O(1).
This is still a strict improvement over O(n) for all n ≥ 2, but is suboptimal compared to
a hash set. The tradeoff:

- **Hash set (O(1)):** requires ``Hash`` + ``Eq`` trait bounds; no element ordering
- **BST set (O(log n)):** requires only ``Ord``; provides sorted iteration
- **List (O(n)):** requires only ``Eq``; provides insertion-order iteration

For the visited/onStack use case, the ordering provided by BST sets is never needed — hash
sets are always the correct fix. In languages where hash sets require an additional trait
bound not already on the node type (e.g., Haskell ``Hashable``), BST sets with ``Ord`` are
an acceptable intermediate fix.

Four Canonical Fix Patterns
-----------------------------

**Python:**

.. code-block:: python

   # Before
   visited = []
   if node in visited: ...

   # After
   visited = set()
   if node in visited: ...

**Java:**

.. code-block:: java

   // Before
   List<Node> visited = new ArrayList<>();
   if (visited.contains(node)) ...

   // After
   Set<Node> visited = new HashSet<>();
   if (!visited.add(node)) ...   // add() returns false if already present

**Haskell:**

.. code-block:: haskell

   -- Before (O(n))
   if v `elem` visited then ...

   -- After with Data.Set (O(log n))
   if Set.member v visited then ...

   -- After with Data.HashMap (O(1))
   if HashMap.member v visited then ...

**Erlang:**

.. code-block:: erlang

   %% Before (O(n))
   case lists:member(V, Visited) of ...

   %% After with gb_sets (O(log n))
   case gb_sets:is_member(V, Visited) of ...

   %% After with maps (O(1))
   case maps:is_key(V, Visited) of ...

Semantic Preservation
----------------------

The fix is semantically identical to the original in all confirmed defect sites because:

1. The visited/onStack set **never contains duplicates by construction** — elements are added
   exactly once and never added if already present
2. Therefore, set membership returns the identical boolean as list membership for all inputs
   that occur in practice
3. The patch changes only the **representation** of the set, not the **semantics** of membership

This is proven by the unit tests: for all tested inputs, the patched and original implementations
produce identical output (same SCCs, same topological orders, same cycle-detection results).
Only performance differs.