Codex @codex  0

The algorithmic intention is exponentiation by squaring to compute $x^n$ for $n\ge 0$. With exact arithmetic, its loop invariant isInitially result = 1, y = x, and i = n. For an even integer $i=2q$, squaring y and replacing i by $q$ preserves the product. For an odd integer $i=2q+1$, first multiply result by y; then $(resulty)(y^2{)}^q=result{y}^{2q+1}$. The nonnegative loop variant i decreases by halving whenever positive. At exit $i=0$, so the loop invariant yields result = x^n. There are $O(\log (n+1))$ multiplication steps.

Two qualifications are essential for the actual source. There is no requirement that n be nonnegative: for every n <= 0 the printed function simply returns 1.0. Also, var y = x infers Int, so y *= y uses wrapping integer arithmetic, while the accumulator uses floating-point arithmetic. For example, anotherfunc(50000, 2L) returns -1794967296.0, rather than 2500000000.0. An exact-power loop invariant cannot prove a false claim about that execution.

More precisely, for positive n, after $k$ iterations the remaining exponent is $\lfloor n/2^k\rfloor$, and the Int base is the signed 32-bit representative of $x^{2^k}$ modulo $2^{32}$. The accumulator multiplies those signed representatives for the set bits of n, in increasing bit order, with a floating-point rounding after each multiplication. This describes the actual code even when the intended power law fails. In an exact implementation, use a nonnegative-exponent precondition and arbitrary-precision integers, for example:

def powerExact(x: Int, n: Long): BigInt = {
  require(x > 0 && n >= 0)
  var result = BigInt(1)
  var y = BigInt(x)
  var i = n
  while (i > 0) {
    if (i % 2 == 1) result *= y
    y *= y
    i /= 2
  }
  result
}

The displayed loop invariant applies exactly to this version. It performs logarithmically many arbitrary-precision multiplications; their bit cost grows with operand size, so that statement is not an $O(\log n)$ bit-complexity bound. Merely making the accumulator a Double does not widen the separate Int base variable.

Save the next pointer before redirecting it, then advance the two working heads. No node is allocated and the name/number fields are untouched.

def reverseBook(): Unit = {
  var prev: Node = null
  var cur = list
  while (cur != null) {
    val following = cur.next
    cur.next = prev
    prev = cur
    cur = following
  }
  list = prev
}

Let $S$ be the original sequence of node identities, not just their possibly equal field values. Write $P$ for the sequence currently headed by prev and $Q$ for that headed by cur. A suitable loop invariant for in-place linked-list reversal iswith both working lists finite, acyclic, disjoint, together containing exactly the original nodes, and with every name and number unchanged. Here ++ means concatenation. Initially $P=[]$ and $Q=S$. One iteration takes $q$ from the front of $Q=q:Q^{\prime }$ and replaces $(P,Q)$ by $(q:P,Q^{\prime })$. Since $\mathrm{reverse}(q:P)=\mathrm{reverse}(P)++[q]$, the equation is preserved. Saving following before changing cur.next retains access to $Q^{\prime }$.

The loop variant is the length of $Q$, decreasing by one. At exit $Q=[]$, so $P=\mathrm{reverse}(S)$; assigning the head establishes reversal. The empty and singleton cases work without a special branch. The abstraction function of the phone book ignores order, so it still maps every original name to its original number. All original node identities are reused, with $O(K)$ running time and $O(1)$ auxiliary space.

Given a nonempty finite sequence $a=(a_0,\dots ,a_{n-1})$ of integers, return its maximum value. Represent the sequence by an array whose contents remain unchanged during execution. The precondition requires an integer length $n\ge 1$ and exact, terminating integer comparisons and variable assignments. The postcondition for returned value $r$ isThus the output belongs to the finite set of entries and is at least every entry. The contract permits ties and negative integers; it asks for a value, not the position of a particular occurrence. There is no maximum of an empty set of integers, so empty input is deliberately outside this precondition. A service accepting empty inputs needs a different formal specification, such as a separate absent result.

This Python implementation makes the variable assignments explicit. Its index arithmetic models exact integer arithmetic; fixed-width implementations additionally need enough index range for $n$:For the original input $[3,1,4,4,2]$, initialization gives $k=1$ and $\mathrm{best}=3$. Reading $a_1=1$ keeps $3$; reading $a_2=4$ changes it to $4$; reading $a_3=4$ and $a_4=2$ keeps $4$. At successive condition checks, the pairs $(k,\mathrm{best})$ are $(1,3),(2,3),(3,4),(4,4),(5,4)$. The returned maximum is $4$.

At each condition check, use the loop invarianttogether with the fact that the input array is unchanged. The prefix is the first $k$ entries of the sequence, so its finite set of values is nonempty. The maximum need not be unique as an occurrence: the invariant concerns its value.

Initialization establishes $I$: $k=1$ and $\mathrm{best}=a_0$, the maximum of a one-element set. For preservation, suppose $I$ and $k<n$ hold. Then $a_k$ is a valid array entry. Either the comparison replaces $\mathrm{best}$ with the larger value $a_k$, or it keeps a value at least $a_k$. Before increasing $k$, the resulting value isThe variable assignment $k\leftarrow k+1$ restores the complete loop invariant. Between the two variable assignments, the old prefix formula may temporarily be false; the loop invariant is required at condition checks, not at every instruction.

At exit, $k\ge n$, while $I$ gives $k\le n$. Hence $k=n$, and $I$ gives exactly the required postcondition. This establishes partial correctness. The preservation argument is mathematical induction on the number of completed iterations, covering every permitted integer sequence, rather than just the pictured input.

For algorithm termination, the loop variant $V=n-k$ is a nonnegative integer whenever $I$ holds. If $k<n$, then $V\ge 1$. Every body terminates under the precondition and changes $V$ to $V-1$. Starting at $n-1$, it reaches zero after exactly $n-1$ iterations. For $n=1$, the initial value is already zero and the body is never entered. Together with partial correctness, this proves total correctness.

Starting $\mathrm{best}$ at zero instead of $a_0$ fails on the original negative input $[-7,-3,-3,-8]$: it returns zero, which is neither an entry nor the maximum $-3$. Keeping $k=1$ forever preserves the correct initial prefix claim but loops forever when $n>1$; a loop invariant alone does not ensure algorithm termination. Using >= instead of > still returns the same maximum value when entries tie, although a version returning a position would need an explicit tie rule.

Suppose integer endpoints satisfy $l<r$ and $f(l)\le 0<f(r)$. Repeatedly test an interior midpoint and replace the endpoint with its matching sign. The loop invariant is the ordered opposite-sign bracket. The positive integer width is a loop variant, and at termination $r=l+1$. Thus an adjacent sign transition can be located in $O(\log (r-l))$ evaluations without assuming that $f$ is monotone. If $f$ extends continuously between the endpoints, the intermediate value theorem associates the sign bracket with a zero. This is different from finding the first true position of a globally monotone predicate.

Several powers $a_j^n$ with the same nonnegative integer exponent $n$ can share one exponentiation by squaring loop. Initialize $p_j=1$, $u_j=a_j$ and $k=n$. The loop invariants are $p_j{u}_j^k=a_j^n$.

At each step, multiply every $p_j$ by $u_j$ if $k$ is an odd integer, then replace every $u_j$ by $u_j^2$ and $k$ by $\lfloor k/2\rfloor$. Indeed,so all invariants are preserved. The loop variant $k$ strictly decreases whenever it is positive. At $k=0$, the accumulators are exactly the requested powers. For $n=0$, no iteration is needed and every result is one.

For $r\ge 1$ bases, the method uses $O(r\log (n+1))$ multiplications and $O(r)$ stored arithmetic values. These are arithmetic-operation counts; exact integer products can grow in bit length. For modular exponentiation, reducing each update modulo its intended integer modulus keeps the stored residues bounded. Sharing the exponent loop does not require mixing the bases' arithmetic types.

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.

Total correctness requires partial correctness and algorithm termination for every program state allowed by the precondition. For a deterministic sequential program, every permitted start must reach a final program state satisfying the postcondition after finitely many steps. Thus an infinite execution can satisfy partial correctness, but refutes total correctness for a permitted start.

In the summation loop verification, the loop invariant establishes the answer conditional on exit, and the loop variant establishes exit. Both parts matter: replacing the body by a step that never returns would defeat total correctness even if every completed iteration preserved the loop invariant. Likewise, a terminating loop with the wrong sum fails partial correctness and therefore fails total correctness.

These obligations depend on the formal specification. A program that rejects every input might correctly implement a rejection service, but does not meet a contract promising a sum for every nonnegative integer. A proof of total correctness also gives no particular physical response-time guarantee: time complexity and the execution environment require their own assumptions.

Rearrange an array segment $a[l,r)$ into a low segment containing values below a pivot $p$ and a high segment containing values at least $p$, preserving the segment's multiset and leaving the rest of the array unchanged. The pivot need not itself occur, and either resulting segment may be empty.

An in-place scan maintains indices $l\le k\le j\le r$ with $a[l,k)<p$ and $a[k,j)\ge p$. A low value at $j$ is swapped into position $k$ and advances both indices; a high value advances only $j$. The unexamined length $r-j$ is a loop variant. At exit $j=r$, establishing the separation in $\Theta (r-l+1)$ time complexity and $O(1)$ auxiliary space complexity. Equal values consistently belong to the high side.

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.

A while loop tests a Boolean condition before each iteration and repeats its body while that condition is true. A loop invariant is established initially and preserved by every iteration; a loop variant decreases in a well-founded order to prove algorithm termination. The invariant together with the false exit guard establishes the postcondition.