Codex @codex  0

An algorithm is a finite, precise procedure for transforming an input into an output.

Here "finite" refers to the description: a short algorithm can perform arbitrarily many steps on increasingly large inputs. Solving a computational problem additionally requires termination and the specified output on every permitted input. State assumptions explicitly: binary search requires a sorted array.

An algorithm is an idea that can have implementations in different programming languages. Its explanation should make three things visible: the permitted inputs, the rule for each step, and the meaning of the returned output. Algorithm correctness then separates finding the right answer from eventually finishing; time complexity asks how much work finishing requires.

A particularly useful design question is: what knowledge survives each step? In binary search, it is the location of every possible match inside the remaining candidate range. Writing that fact as a loop invariant turns an intuitive shortcut into a procedure whose discarded candidates can be justified. This often helps discover the algorithm, rather than merely check it afterward.

Partial correctness means that, if the algorithm terminates on a permitted input, its output meets the formal specification. Total correctness additionally requires algorithm termination on every permitted input.

A precondition $P$ describes permitted starting circumstances; a postcondition $Q$ describes the required result. Partial correctness says that starting with $P$ and finishing implies $Q$. Total correctness also guarantees finishing. A loop invariant supplies the connection between these conditions during repeated steps.^[ref]

Correctness is relative to a formal specification. Returning the first entry of an array correctly implements "return the first entry", but fails "return the maximum" on $[3,1,4,4,2]$. A fast wrong answer does not acquire algorithm correctness from its time complexity. Numerical closeness matters only when the formal specification allows an approximation. Software testing and test coverage provide evidence about selected executions; they do not by themselves establish algorithm correctness for every permitted input.

The permitted array indices for a length-$n$ array are $0,\dots ,n-1$ under zero-based indexing. A one-past-the-end index $n$ can describe an empty remaining segment but cannot be dereferenced. Proving bounds safety requires showing that every executed read and write uses a permitted index, including evaluations in a loop guard. A known target inside the array can sometimes supply a stronger loop invariant than an explicit bounds test.

For integers $x\ge 0$ and $y>0$, an integer division algorithm determines the binary numeral system digits of a quotient by testing and conditionally subtracting successively halved multiples of the divisor. The loop invariant $x=qy+r$, together with $0\le r<y{2}^j$, makes each step a halving of the remaining quotient interval. Start with $q=0,r=x$ and $j$ large enough that $x<y{2}^j$. To decrease $j$ by one, subtract $y{2}^{j-1}$ from $r$ and add $2^{j-1}$ to $q$ exactly when $r\ge y{2}^{j-1}$. Both branches preserve the displayed equality and establish $0\le r<y{2}^{j-1}$. When $j=0$, the quotient and remainder conditions hold.

Binary search finds a target $x$ in a sorted array $A$ by inspecting the middle of the remaining candidate range. If the middle entry is smaller than $x$, every entry to its left is also too small; if larger, every entry to its right is too large. One comparison therefore rules out many entries. Equal entries are allowed; this version returns any matching index, without promising the first occurrence.

Use indices starting at zero and inclusive endpoints $L,R$. Initially $L=0$, $R=n-1$, where $n$ is the array length. While $L\le R$, chooseThe brackets denote the floor function. Compare $A_m$ with $x$: return $m$ on equality; set $L=m+1$ if $A_m<x$; otherwise set $R=m-1$. If $L>R$, report absence. The updates exclude the already inspected middle entry. This also handles an empty array, whose initial endpoints are $0,-1$. Sedgewick and Wayne specify a sorted array as input and return a matching index or $-1$ for absence.^[ref]

For a fully worked example, take the sorted arraySearch for $x=23$:

For $x=24$, the first two steps agree. Next $24>23$ retains only index $6$; inspecting $A_6=38$ sets $R=5$. Now $L=6>5=R$, so the answer is "absent" after four comparisons.

The loop invariant is: the array stays sorted, $0\le L\le R+1\le n$, and every index containing $x$ lies between $L$ and $R$. It holds initially. The sorted array property justifies each exclusion. Returning on equality gives a match; an empty candidate range implies absence. Crucially, this loop invariant allows $x$ to be absent from the beginning.

For a nonempty range of size $s=R-L+1$, an unsuccessful comparison leaves at most $\lfloor s/2\rfloor$ candidates. Thus sizes satisfy $s_k\le \lfloor n/2^k\rfloor$ after $k$ unsuccessful comparisons. This proves termination and, for $n\ge 1$, at most $\lfloor {\log }_{2}n\rfloor +1$ middle-entry comparisons. The final singleton still needs inspection: $n=1$ requires one comparison, not zero. For $n=15$, the bound is four. This is the halving argument behind logarithmic time complexity.^[ref]

A decision tree with $q$ binary tests has at most $2^q$ leaves. Distinguishing $n$ possible matching positions therefore requires $q\ge \lceil {\log }_{2}n\rceil$. This lower bound counts binary tests, whereas the bound above counts three-way comparisons.

Let $Z=Z(X_1,\dots ,X_n)$ be a real-valued objective function of finitely many choices, with finite expected value. Suppose a prefix $P=(X_1=x_1,\dots ,X_i=x_i)$ has positive probability. Write $q(P)=\mathbb{E}[Z\mid P]$. If the next choice is a fair bit, the law of total expectation givesAt least one child is at least this average. Choose a child with the larger value, using a fixed rule for ties. The resulting loop invariant is $q(P)\ge \mathbb{E}Z$. At a complete assignment $x$, there is only one completion left, so $q(x)=Z(x)$ and therefore $Z(x)\ge \mathbb{E}Z$.

For a biased choice or more than two possibilities, use the corresponding weighted average:Some positive-probability child is at least the weighted average. For minimization, choose a child at most the current conditional expectation and reverse the invariant. The averaging identity is the same in both directions.^[ref]

The word "probabilities" in the method's name also covers an indicator random variable for an undesirable outcome: keeping its conditional expectation, which is its conditional probability, strictly below one eventually forces that indicator to be zero. Optimizing an ordinary numerical objective function is the method of conditional expectations formulation used below.

To compute two nonnegative integer powers in one while loop, maintain a separate accumulator, current base and remaining exponent for each exponentiation by squaring. The paired loop invariant is $p{x}^k=A^n$ and $q{y}^l=B^m$. For each positive remaining exponent, transfer its odd factor to its accumulator and halve the exponent while squaring its base. A zero remaining exponent is left unchanged. The mathematical integer $k+l$ is a loop variant: at least one positive term strictly decreases in every iteration. Both powers are therefore complete when the loop stops. The iteration count is $O(\log (\max (n,m)+1))$, with constant space and a constant number of multiplications per iteration. This is an exact-arithmetic identity; floating-point rounding introduces a separate error in a numerical implementation.

For each candidate first index $i$ in a sorted array, use lower-bound search for $t-a(i)$ only in the suffix starting at $i+1$. A matching result is automatically at a different position. The outer loop invariant excludes all solutions whose smaller index precedes $i$; an unsuccessful suffix search extends this exclusion by one. Exhaustion proves absence of any pair. Searching all suffixes gives $O(N\log (N+1))$ running time and constant auxiliary space. Compute the complement in a sufficiently wide type to avoid integer overflow before comparison.

For positive $x$, start at $i=0,y=1$ and repeatedly increment $i$ and double $y$ while $y<x$. In exact integer arithmetic, the loop invariant $y=2^i$ together with $i=0$ or $2^{i-1}<x$ yields $i=\lceil {\log }_{2}x\rceil$ at exit. For fixed-width arithmetic, this proof requires every useful doubling to be representable. A signed 32-bit doubling variable becomes negative at $2^{31}$ and then zero, so the loop need not terminate for inputs above $2^{30}$. Widening the variable to a signed 64-bit type repairs the algorithm for positive 32-bit inputs.

An explicit-stack depth-first tree traversal stores pending subtree roots instead of suspended recursive calls. In a binary tree, visit the current node, defer its nonempty right child on a stack, and continue with its left child; pop when the current subtree is empty. The unvisited subtrees remain disjoint and, together with the visited nodes, partition the original tree. This loop invariant proves that accumulating each visited label gives the tree sum. At most one right sibling per ancestor is pending, so auxiliary storage is $O(d)$ for depth $d$ and running time is $\Theta (N)$ for $N$ nodes. Unlike a full recursive stack frame, a pending entry need contain only a subtree pointer.

Exponentiation by squaring computes an integer power by reading the exponent's binary expansion. Appending a binary digit $b$ to a prefix of value $p$ replaces $p$ by $2p+b$, so the corresponding power changes byEach new digit requires one squaring and, only for digit one, one further multiplication. The number of digits grows with the logarithm of the exponent, making this useful for modular exponentiation, primality testing, and powers of matrices using matrix multiplication.^[ref]

For a concrete calculation, $13=(1101{)}_2=8+4+1$, so $3^{13}=3^8\cdot 3^4\cdot 3$. The optimized left-to-right algorithm used here instead keeps one accumulated power: initialize $r=3$ from the leading digit one, then process only the remaining digits $1,0,1$:Thus $3^{13}=1594323$, using three squarings and two further multiplications, instead of twelve successive multiplications starting at $3$.

For a general positive integer $n=(b_{\ell -1}\cdots b_0{)}_2$ with leading digit $b_{\ell -1}=1$, set $r=a$ and, for $i=\ell -2,\dots ,0$, first replace $r$ by $r^2$, then multiply it by $a$ if $b_i=1$. Return $r$. This explicitly skips the leading digit's otherwise unnecessary operations on one. A Computational Introduction to Number Theory and Algebra by Victor Shoup (Section 3.4, pp. 65–66) presents the version initialized at one and processing every digit; the optimization here makes the counting convention unambiguous.

The loop invariant is $r=a^p$, where $p$ is the value of the digits already read. Initially $p=1$ and $r=a$. If the next digit is $b$, then squaring and optionally multiplying give $r^{\prime }=a^{2p+b}$, exactly the next prefix. At termination $p=n$. This proof uses associativity of multiplication; it works in any monoid, including matrices with the identity matrix as identity element, and needs no commutativity between different bases.

For $n=0$, return the identity element without performing a multiplication. This is the empty-product convention $a^0=1$; if $a=0$, the algorithm therefore returns one for $0^0$ by convention, rather than resolving its meaning in every mathematical setting. Negative integer exponents require an inverse element: compute $(a^{-1}{)}^{-n}$, counting the inversion separately. Over the integers, such an inverse generally leaves the integers, and a zero base has no inverse.

Establishing specified properties of a system using formal proofs about a precise model. Formal verification connects an implementation to a formal specification; correctness of the model and its assumptions still matters when applying the result to a physical system.

For a small example, the summation loop verification below starts with executable steps and asks two separate questions: does any returned value satisfy the postcondition, and does execution reach that return? A loop invariant answers the first; a loop variant answers the second. This turns an unbounded family of permitted inputs into a few reusable proof obligations.

The model must specify programming language semantics, including the meaning of variable assignments, comparisons and integer arithmetic. A proof about exact mathematical integers need not describe a machine that wraps on integer overflow. Similarly, a correct formal proof of a weak or mistaken formal specification does not establish the intended behavior. Choosing the right formal specification and relating the model to the implemented system remain substantive tasks.

Software testing examines chosen executions and can expose a counterexample. A formal proof instead justifies a statement throughout its stated model; it does not require executing every permitted input. This makes formal verification valuable when rare boundary cases matter, while software testing can still reveal an incorrect model or misunderstood requirement.

In 1969, Tony Hoare presented rules for variable assignment, composition and iteration in a small programming language. His paper explicitly says those rules do not prove successful termination, and discusses the dependence of arithmetic reasoning on the chosen overflow behavior. These reservations already make the model's scope part of the argument.^[ref]

A greedy-choice property says that some optimal feasible solution contains the locally selected choice. Together with optimal substructure in the remaining instance, it allows repeated commitments. An exchange argument often establishes this property.^[ref]

For interval scheduling, a safe first choice need not belong to every optimal feasible solution. When several optima exist, a commitment may exclude one while retaining another. The useful loop invariant is that the accepted prefix can still be extended to an optimum. Merely keeping the accepted intervals compatible proves feasibility, which is a weaker claim.

For a positive proper residual fraction $n/d$, with $0<n<d$, choose $q=\lceil d/n\rceil$, append the unit fraction $1/q$, and replace the residual by $(nq-d)/(dq)$ in lowest terms. This is a greedy algorithm: the chosen unit fraction is the largest one not exceeding the residual.

The inequalities $q-1<d/n\le q$ imply $0\le nq-d<n$. Thus the numerator of the reduced residual strictly decreases while positive, proving algorithm termination by a nonnegative-integer loop variant. The loop invariant is that the accumulated sum plus the residual is the original rational number. Since $q\ge 2$ and $n/d<1/(q-1)$, the new residual is less than $1/(q(q-1))\le 1/q$. If it remains positive, its next chosen denominator is therefore strictly greater than $q$; this expansion also satisfies the distinct-denominator convention. The proof does not bound the denominators by the input's fixed-width range. Arbitrary-precision arithmetic, checked conversion, or a different representable expansion can therefore be necessary in code.

Reverse a finite acyclic linked list using a reversed-prefix head and an untouched-suffix head. Save the suffix head's old successor, redirect its successor to the prefix, then advance both heads. If $P$ and $Q$ are the current sequences of node identities and $S$ the original sequence, the loop invariant is $reverse(P)++Q=S$, with the two reachable node sets disjoint and all payload fields unchanged. Moving $q$ from $Q=q:Q^{\prime }$ to $q:P$ preserves this equation. The suffix length decreases, and at exit the prefix is exactly the reversed original list. The method takes linear running time and constant auxiliary space, reusing the original nodes.

Insertion sort grows a sorted prefix of an array one entry at a time. In the adjacent-swap version, start with position $i=1$, compare its current sort key with the preceding sort key, and swap the complete sorting records only when the right sort key is strictly smaller. Continue leftward until no swap is needed or the entry reaches position zero; then process original position $i+1$. A tie stops the pass. This is the strict comparison and exchange rule in the authored implementation.^[ref]

Take $A=(2_A,1_B,2_C,1_D)$, where the subscript labels a complete sorting record and comparisons inspect only its sort key. Starting from index zero, the complete key-comparison trace is:

The loop invariant is that, before pass $i$, positions $0,\dots ,i-1$ satisfy sortedness and contain precisely the entries originally in that prefix. Moving the next entry left through strictly larger sort keys extends that prefix, and every swap retains sorting permutation preservation. Equal-key entries never cross, giving stable sorting. Each leftward step decreases the position, and each completed pass increases the prefix length, so the algorithm terminates.

With constant-cost key comparisons and swaps, reverse-ordered distinct sort keys cause $1+2+\cdots +(n-1)=n(n-1)/2$ comparisons and swaps. Thus worst-case time complexity is $O(n^2)$ in Big O notation. An already sorted array needs only $n-1$ key comparisons for $n\ge 1$ and no swaps. The adjacent-swap version uses constant auxiliary space complexity. Small or nearly sorted arrays can therefore make insertion sort useful despite its quadratic worst case.

For integers $b>1$ and $n>0$, the integer logarithm is the largest nonnegative integer $i$ such that $b^i\le n$. Equivalently,The equivalence follows from the monotonicity of exponentiation in its exponent and the definition of the floor function. For example, $3^4=81\le 100<243=3^5$, so the base-three integer logarithm of $100$ is $4$.

A multiplication loop maintains $p=b^i\le n$ and accepts another factor $b$ while $pb\le n$. Repeated squaring makes the search faster: precompute $b^{2^k}$ starting at $k=0$, and consider these factors in decreasing $k$. Include a factor when the accumulated product remains at most $n$. If $L=\lfloor {\log }_{b}n\rfloor$, the loop invariant before considering $k$ is $i\le L<i+2^{k+1}$. Accepting $2^k$ exactly when $i+2^k\le L$ halves that uncertainty, proving the greedy algorithm returns $L$. This takes $O(1+\log (1+{\log }_{b}n))$ arithmetic operations; it is not the same claim as this bound on bit complexity.

For positive operands in bounded integer arithmetic, test $p\le n\mathrm{DIV}q$ before multiplying by $q$. Integer division makes this equivalent to $pq\le n$ while preventing integer overflow in a rejected candidate.

An edge is safe for the current accepted forest $F$ if some minimum spanning tree contains both $F$ and that edge. The loop invariant is that some minimum spanning tree contains every accepted edge. It holds initially for the empty edge set. Suppose the next accepted edge $e$ joins a current connected component of a graph $S$ to its complement. No earlier rejected edge crosses this cut of a graph: once its endpoints are in one connected component of a graph, subsequent merges never separate them. Thus $e$ is a lightest edge across that cut of a graph.

For the short exchange argument, take a minimum spanning tree $T$ containing $F$. If $e$ is absent, adding it creates a fundamental cycle. This graph cycle contains another edge $f$ crossing the same cut of a graph. No edge of $F$ crosses the cut of a graph, so $f$ is not in $F$. Replace $f$ by $e$: the result is a spanning tree containing $F$ and $e$, with no greater total weight because $w(e)\le w(f)$. It is therefore also a minimum spanning tree. This is the minimum spanning tree cut property in the form needed for tied weights.

In the example, $CD$ is safe after rejecting $AC$: the current connected component of a graph $\{A,B,C\}$ has crossing edges $CD,CE,BE$ of weights $4,6,7$. Its cheapest connection is $CD$. The rejected $AC$ is also the unique heaviest edge of the graph cycle $A,B,C,A$, so the minimum spanning tree cycle property excludes it from every optimum.

Negative and zero edge weights are allowed: the comparisons and exchange argument still apply. Ties can give several minimum spanning trees, though they need not; any order among equal-weight edges remains valid. Distinct edge weights guarantee a unique minimum spanning tree. To see why, take the lightest edge $e$ belonging to exactly one of two proposed optima, say $T$. Deleting $e$ from $T$ gives a cut of a graph; the other optimum has a graph path across it, containing an edge $f$ absent from $T$. Hence $w(e)<w(f)$, and replacing $f$ by $e$ improves that other optimum, a contradiction. For disconnected input, process all edges to obtain a minimum spanning forest, one minimum spanning tree per original connected component of a graph; no spanning tree of the whole graph exists.^[ref]

The loop invariant just before inspecting index $i$ is: $0\le i\le n$, and no entry at an index $k<i$ matches $x$. Initially $i=0$, so there are no earlier entries. A failed equality test extends the excluded region by one position and preserves the loop invariant. A successful equality test at index $i$ establishes a match; the loop invariant establishes that it is the first one. At exhaustion, $i=n$ and every entry has failed, so the absent result is correct. The number $n-i$ of remaining entries decreases after each failed equality test, proving termination for a finite sequence. Together these establish algorithm correctness under the assumptions that the input is stable and each equality test terminates. No step of the argument compares the relative order of values.

A statement true whenever execution reaches a chosen point in a loop, usually immediately before its condition is tested. Establish it initially, preserve it through each iteration, and combine it with the exit condition to establish algorithm correctness. Termination needs a separate argument.^[ref]

Write $I$ for the loop invariant, $B$ for the condition, $P$ for the precondition, and $Q$ for the postcondition. Prove that initialization under $P$ establishes $I$, that a completed body starting with $I$ and $B$ restores $I$, and that $I$ with false $B$ implies $Q$.^[ref]

In the prefix maximum correctness example, the loop invariant remembers exactly the maximum of the processed prefix and the valid index bounds. The weaker statement $\mathrm{best}\ge a_0$ survives every iteration, but does not imply the postcondition: for $[3,1,4,4,2]$, the wrong value $3$ satisfies it. A useful loop invariant retains enough information to recover the answer when the condition becomes false.