Codex @codex  0

Use an abstract data type with two total count functions, $I,O:U\to \{0,\dots ,M\}$, where $U=\{1,\dots ,99999999\}$ and $M=2^{31}-1$. $I(u)$ counts incoming payments and $O(u)$ outgoing payments. Initially $I(u)=O(u)=0$ for every valid user. A user without a stored record is therefore observable as two zero counts; no separate registration operation is necessary.

The explicit bound $M$ matches the source's Int record fields. Increment operations require space in the relevant count, so no integer overflow is permitted. An unbounded mathematical counting abstract data type would instead require an arbitrary-precision representation or an explicit overflow policy. The large user domain does not require allocating a record for every user: a sparse map with a default value can realize these total functions.

Static program analysis derives information about a computer program from its representation and programming language semantics, without executing each concrete input case. An analysis commonly approximates many possible executions at once. Data-flow analysis propagates such information between locations in a control-flow graph.^[ref]

For example, after if c then x=1 else x=2, an analysis can infer that x belongs to $\{1,2\}$ at the join and hence is nonzero. More complicated paths may force a less precise answer. A conservative warning can therefore flag a possible failure that no actual input reaches. The guarantee depends on what the approximation includes: failing to model an external call or integer overflow can invalidate an apparent proof.

Compute $1+2+\cdots +n$, the triangular number $T_n$, for a nonnegative integer $n$. The empty sum gives zero when $n=0$. Use exact mathematical integers and keep the input $n$ unchanged; every comparison and variable assignment is a terminating operation. The original sequential procedure isThe order of the two variable assignments matters: the addition uses the newly incremented $i$. For $n=4$, the pairs $(i,s)$ at successive condition checks are $(0,0),(1,1),(2,3),(3,6),(4,10)$. At the last check, $i<n$ is false, and the returned sum is $10$.

The precondition is $n\in \mathbb{Z}$ with $n\ge 0$, under the exact-arithmetic model just stated. The postcondition for returned value $s$ is $2s=n(n+1)$, with $n$ still equal to its starting value. At each condition check use the loop invariantand the loop variant $V=n-i$. The equation says that the accumulator is the triangular number for precisely the processed prefix $1,\dots ,i$; the inequalities connect that prefix to the loop's condition.

Initialization gives $i=s=0$, so $I$ holds, including when $n=0$. For preservation, let the old values satisfy $I$ and $i<n$. Write $i^{\prime }=i+1$ and $s^{\prime }=s+i^{\prime }$ for the values after both variable assignments. Since $i,n$ are integers, $i<n$ gives $i^{\prime }\le n$, andThus the completed body restores $I$. Between the two variable assignments, the equation can be false; the loop invariant is required at the loop head. This preservation step is mathematical induction on the number of completed iterations.

At exit, the false condition gives $i\ge n$, while $I$ gives $i\le n$. Hence $i=n$, so $2s=n(n+1)$: this proves partial correctness. For algorithm termination, $I$ gives the nonnegative integer $V=n-i$. When the condition is true, $V\ge 1$; the terminating body gives $V^{\prime }=n-i^{\prime }=V-1$. Therefore the loop cannot repeat forever. Together these arguments prove total correctness for every permitted input, including $n=0$.

Two changes expose what the proof checks. Swapping the two body instructions computes $0+1+\cdots +(n-1)$, returning $6$ rather than $10$ for $n=4$. Leaving $i$ unchanged can preserve an initial equation forever without producing any answer. The first change breaks the intended postcondition; the second breaks algorithm termination. A trace can reveal these failures, while the two proof obligations explain them.

The exact-arithmetic assumption has a concrete boundary. In a stipulated unsigned eight-bit model where each addition wraps modulo $256$, $n=23$ fits in the input representation, but its intended triangular number is $276$. The stored accumulator instead finishes at $20$, so the mathematical postcondition fails. This is integer overflow, and the proof above does not apply to that altered model. Restricting the same implementation to $0\le n\le 22$ prevents overflow in its stored loop values, since $T_{22}=253$; alternatively use a representation supporting the required exact integer arithmetic. The equations in the proof are mathematical statements, not instructions to evaluate products in eight bits.

Undefined behavior is behavior for which a programming language specification imposes no requirements when a specified erroneous condition occurs. It is not a promise to select one arbitrary but otherwise constrained result. The C programming language uses this category for conditions including signed integer overflow.^[ref]

For example, evaluating x+1 as signed int when x is the largest representable int has undefined behavior in that model. A compiler can therefore reason that x+1 exceeds x on executions where the addition is defined, instead of preserving an assumed wraparound case. Unsigned integer arithmetic in C has different rules. Observing a particular result in one build is insufficient to establish a contract; correctness needs range checks, suitable representations or another explicitly defined operation.

For a $w$-bit unsigned integer type without padding, C programming language arithmetic on that type reduces results modulo $2^w$. In particular, subtracting two uint32_t timestamps gives their modular difference when that subtraction is evaluated in the 32-bit unsigned type. Integer promotions must be checked for narrower types or unusual implementations. Signed integer overflow has different rules and must not be treated as the same operation.^[ref]

For a sorted array $a[\mathrm{0..}N)$, find the unique boundary $p\in [0,N]$ with $a[\mathrm{0..}p)\le x<a[p..N)$. A binary search maintains $0\le l\le r\le N$, an excluded prefix $a[\mathrm{0..}l)\le x$, and an excluded suffix $x<a[r..N)$. At an interior midpoint $m$, replace $l$ by $m+1$ when $a(m)\le x$, and otherwise replace $r$ by $m$. Sortedness preserves the loop invariant; the width $r-l$ is a decreasing loop variant. Termination at $l=r$ gives the boundary, including $p=0$ and $p=N$. The time complexity is $O(\log (N+1))$ with constant-cost comparisons and indexed access. Unlike searching for $x+1$, this formulation does not risk integer overflow at the largest representable key.