Proofs: Dynamic array

Append and pop on a dynamic array cost O(1) amortized full

This proof shows: amortized.

Cost model. APPEND costs 1 for line L2, plus $n$ if line L1 resizes. POP costs 1 for line L5, plus $n'$ if line L6 resizes, where $n' = n - 1$ is the count after line L4. RESIZE costs one unit per copy in line L10. GET and SET cost 1 and do not change $n$ or $cap$.

Potential. For a state with count $n$ and capacity $cap$, let

Both branches are at least 0 where they apply, so $\Phi \ge 0$. At the start $\Phi(0, 1) = 1/2$. The amortized cost of an operation is its cost plus $\Phi_{\text{after}} - \Phi_{\text{before}}$.

Claim. Each APPEND has amortized cost at most 3, and each POP at most 2.

APPEND without a resize ($n < cap$). The cost is 1 and $n$ becomes $n + 1$.

• If $2n \ge cap$: $\Delta\Phi = 2(n + 1) - 2n = 2$, amortized cost 3.
• If $2(n + 1) < cap$: $\Delta\Phi = -1$, amortized cost 0.
• If $2n < cap \le 2n + 2$: $\Delta\Phi = (2n + 2 - cap) - (cap/2 - n) = 3n + 2 - \tfrac{3}{2} cap$. Since $cap > 2n$, this is less than $3n + 2 - 3n = 2$, so the amortized cost is less than 3.

APPEND with a resize ($n = cap \ge 1$). The cost is $1 + n$. Before, $\Phi = 2n - n = n$. After, the count is $n + 1$ and the capacity $2n$, and $2(n + 1) \ge 2n$, so $\Phi = 2(n + 1) - 2n = 2$. The amortized cost is $1 + n + 2 - n = 3$.

POP without a resize. The cost is 1 and $n$ becomes $n' = n - 1$, with the same $cap$.

• If $2n' \ge cap$: $\Delta\Phi = -2$, amortized cost $-1$.
• If $2n < cap$: $\Delta\Phi = (cap/2 - n + 1) - (cap/2 - n) = 1$, amortized cost 2.
• If $2n' < cap \le 2n$: $\Delta\Phi = (cap/2 - n + 1) - (2n - cap) = \tfrac{3}{2} cap - 3n + 1$. Since $cap \le 2n$, this is at most $3n - 3n + 1 = 1$, so the amortized cost is at most 2.

POP with a resize ($n' \ge 1$ and $cap = 4n'$). The cost is $1 + n'$. After, the capacity is $2n'$ and the count $n'$, so $\Phi = 2n' - 2n' = 0$. Before, the count was $n' + 1$.

• If $n' \ge 2$: $2(n' + 1) < 4n'$, so $\Phi_{\text{before}} = 2n' - (n' + 1) = n' - 1$, and the amortized cost is $1 + n' + 0 - (n' - 1) = 2$.
• If $n' = 1$: $cap = 4$ and the count was 2, so $2 \cdot 2 \ge 4$ and $\Phi_{\text{before}} = 0$. The amortized cost is $1 + 1 + 0 - 0 = 2$.

This proves the claim. $\square$

Theorem. Any sequence of $m$ operations on a new dynamic array, of which $a$ are appends, costs at most $3a + 2(m - a) + 1/2 \le 3m + 1/2$.

Proof. Let $c_k$ and $\hat c_k$ be the cost and the amortized cost of operation $k$, and $\Phi_k$ the potential after it. Then $\sum_{k=1}^{m} \hat c_k = \sum_{k=1}^{m} c_k + \Phi_m - \Phi_0$, because the sum of the differences telescopes. So $\sum c_k = \sum \hat c_k - \Phi_m + \Phi_0 \le \sum \hat c_k + 1/2$, because $\Phi_m \ge 0$ and $\Phi_0 = 1/2$. GET and SET have amortized cost 1, and the claim bounds the rest. $\blacksquare$

The dynamic array keeps its list and its size bound full

This proof shows: correctness.

Invariant. (I1) $0 \le n \le cap$, and the list held is $(A[0], \ldots, A[n-1])$. (I2) $cap = 2^e$ for some integer $e \ge 0$, and $cap < 4 \max(n, 1)$.

At the start $n = 0$ and $cap = 1 = 2^0 < 4$, so both parts hold for the empty list.

Lemma (RESIZE). If $n \le c$, then RESIZE$(D, c)$ leaves $n$ unchanged, sets $cap = c$, and leaves the list $(A[0], \ldots, A[n-1])$ unchanged.

Proof. Line L8 makes a block $B$ of $c$ cells. The loop of lines L9 and L10 keeps the invariant "$B[k] = A[k]$ for $0 \le k < i$" at its test with value $i$: it holds for $i = 0$, and line L10 extends it to $i + 1$. It runs for $i = 0, \ldots, n - 1$, and each index is less than $c$ because $n \le c$. At exit $B[0 \ldots n-1] = A[0 \ldots n-1]$. Line L11 makes $B$ the block and sets $cap = c$. $\square$

APPEND$(D, x)$. Let $(\ell_0, \ldots, \ell_{n-1})$ be the list before the call, and assume (I1) and (I2).

• If $n < cap$, line L1 does nothing. Line L2 writes $x$ to cell $n < cap$, and line L3 sets the count to $n + 1 \le cap$. The list is $(\ell_0, \ldots, \ell_{n-1}, x)$. The capacity is the same power of two, and $cap < 4\max(n, 1) \le 4(n + 1)$.
• If $n = cap$, line L1 calls RESIZE$(D, 2 cap)$, with $n \le 2 cap$, so by the lemma the list is unchanged and $cap$ becomes $2n = 2^{e+1}$. Now $n < cap$ because $n = cap/2$ and $cap \ge 2$. Lines L2 and L3 append $x$ as in the first case. After the call, $n + 1 \le 2n = cap$ because $n = 2^e \ge 1$, and $cap = 2n < 4(n + 1)$.

In both cases (I1) and (I2) hold for the list with $x$ appended.

POP$(D)$, $n \ge 1$. Let $(\ell_0, \ldots, \ell_{n-1})$ be the list. Line L4 sets the count to $n' = n - 1$, and line L5 reads $x = A[n'] = \ell_{n-1}$, which is in range because $n' < n \le cap$. The list $A[0 \ldots n'-1]$ is $(\ell_0, \ldots, \ell_{n-2})$, and (I1) holds. Line L7 returns $\ell_{n-1}$, the last item. It remains to show (I2) after line L6. Before the call, $cap < 4\max(n, 1) = 4n = 4n' + 4$.

• Case $n' = 0$. Line L6 does nothing. Then $cap < 4 = 4\max(n', 1)$.
• Case $n' \ge 1$ and $4n' = cap$. Line L6 calls RESIZE$(D, cap/2)$. Here $cap = 4n' \ge 4$, so $cap/2 = 2^{e-1}$ is a power of two and is at least $2n' \ge n'$. By the lemma the list is unchanged, and the new capacity is $2n' < 4n'$.
• Case $n' \ge 1$ and $4n' \ne cap$. Line L6 does nothing. If $cap \le 3$, then $cap < 4 \le 4n'$. If $cap \ge 4$, then $cap$ is a multiple of 4, and $cap < 4n' + 4$ gives $cap \le 4n'$; with $cap \ne 4n'$ this gives $cap < 4n'$.

In all cases (I2) holds with $n'$.

GET and SET. These read or write $A[i]$ for $0 \le i < n$, as in an array, and change neither $n$ nor $cap$. $\blacksquare$