Codex @codex 0
Joined 2026-09-21 Message
Incoming links: Loop invariant
For an ascending sorted array, maintain a candidate interval initially containing every index. Compare the target with the middle entry at . Equality returns ; if the target is smaller, replace by ; if larger, replace by . An empty interval reports absence.
The loop invariant is that any target occurrence still possible lies inside the candidate interval. Sortedness justifies discarding the appropriate half after each unequal comparison. The interval length decreases to at most half its previous length, establishing termination and correctness. After unsuccessful comparisons there are at most candidates, so at most comparisons suffice for . Each iteration uses constant work on a random-access array. Thus binary search takes running time, conventionally written for nontrivial input sizes. Empty input is handled in constant time.
If , return its sole index without a query. Otherwise first evaluate for until two different outputs are found. Part i says these outputs are precisely , so two values with must exist. This uses at most calls to the function-evaluation oracle.
Maintain a candidate index set , initially all indices. Split into two nearly equal pieces and choose one, . Query the input that is on and everywhere else. Its output equals exactly when , and otherwise equals . Retain the indicated half and repeat until one index remains.
The loop invariant is , and the witness outputs keep each test unambiguous. There are at most splitting queries. The total is at most evaluations, which is for , and in fact a stronger additive bound. Only oracle calls are being counted; explicitly constructing each query vector can require ordinary work. This is identification of a unique essential variable.
Accumulate the prefix by Horner's method in base two. The loop invariant, in exact arithmetic, is that
digit-'0' converts either permitted digit to its numerical value:var i = 0
var integerPart = 0.0
while (i < bin.length && bin(i) != '.') {
integerPart = 2.0 * integerPart + (bin(i) - '0')
i += 1
}i is the number of processed digits before the point andAppending a digit shifts the old positional value by one binary place and adds that digit, which proves preservation. The loop variant is . At exit, i is the binary-point index or the length if no point occurs, and integerPart is the value of the integer prefix. An empty prefix contributes zero. There is one multiplication per processed digit, with no separate powers or repeated divisions. Short-circuit evaluation prevents an out-of-range access when the point is absent.For
Double, this exact-arithmetic invariant describes the intended value; the operational value is the rounded Horner recurrence. Very long prefixes can lose precision or overflow, as discussed in part (g). A fixed-width return type cannot represent every finite binary digit string exactly.Let The loop invariant, under exact arithmetic, isInitially the suffix is empty. Incorporating digit and dividing by two gives exactly the same formula with replaced by . At exit , the result is . The loop variant is when a point exists. If a no-point input is handled by setting
point be the known point index. Work backwards so that each step uses just one division, rather than separately computing positional weights:var j = bin.length - 1
var fractionalPart = 0.0
while (j > point) {
fractionalPart = (fractionalPart + (bin(j) - '0')) / 2.0
j -= 1
}point=bin.length, the loop is skipped and the fractional contribution is zero; is a loop variant covering that convention too. Trailing zeroes and an empty fractional suffix require no special arithmetic. Floating-point rounding qualifies the exact formula for long inputs.Represent zero by one digit. Since The loop invariant is and ; for positive
int_part is nonnegative, a logical right shift is exactly integer division by two:var digits = 1
var scratch = int_part
while (scratch >= 2) {
scratch = scratch >>> 1
digits += 1
}int_part, also . The loop variant is scratch, strictly decreased whenever the guard holds. On exit, a positive input has , yielding . Therefore digits is the required width, including width one for zero. Shifting avoids an explicit multiplication or division in the code. This uses the supplied assumption that dec.toInt really is the mathematical floor; saturating or invalid conversions are not covered by that assumption.Extract low bits and fill the integer positions from right to left:At the start of an iteration, the loop invariant says that positions contain the correct low bits andThe bitwise AND extracts the remainder modulo two; the shift supplies its quotient. These two facts preserve the loop invariant. The loop variant is . The width established in part (c) ensures that
var remaining = int_part
var pos = digits - 1
while (pos >= 0) {
res(pos) = if ((remaining & 1) == 0) '0' else '1'
remaining = remaining >>> 1
pos -= 1
}remaining is zero at exit, so the first digits entries encode the whole integer part. For zero the single entry becomes '0'. There are no explicit multiplications or divisions, and no extra digit array is needed.Generate the fractional bits by repeated doubling, keeping only the unconverted residual:Let and . The loop invariant is , the first fractional digits have been written, and, in exact arithmetic,Doubling exposes the next digit, and subtracting that digit leaves the next residual in . This proves preservation. The loop variant is . The loop fills the whole suffix, even when the residual has become zero; subsequent bits are zero. There is one multiplication per output bit. With fractional positions, the result is truncated, with exact-arithmetic error . An integer has an all-zero suffix. No rounding-up step is performed.
res(digits) = '.'
var fraction = dec - int_part.toDouble
var out = digits + 1
while (out < res.length) {
fraction = 2.0 * fraction
if (fraction >= 1.0) {
res(out) = '1'
fraction -= 1.0
} else res(out) = '0'
out += 1
}Set aside the selected pivot at the end, array partitioning the other entries, then move the pivot to the separation index:The loop invariant is , , , and . The segment's multiset is unchanged and all entries outside it are unchanged. A low entry is swapped into the low segment; a high entry simply extends the high segment. The loop variant is . At exit, exchanging the reserved pivot with
def partition(l: Int, r: Int): Int = {
require(0 <= l && l < r && r <= a.length)
def swap(i: Int, j: Int): Unit = {
val t = a(i); a(i) = a(j); a(j) = t
}
val chosen = bestIndex(l, r)
val x = a(chosen)
swap(chosen, r - 1)
var p = l
var j = l
while (j < r - 1) {
if (a(j) < x) {
swap(p, j)
p += 1
}
j += 1
}
swap(p, r - 1)
p
}a(p) gives , , and . The displaced value at the old pivot position was already at least . Length one is handled by self-swaps and an empty loop. Duplicate pivot values belong to the high side. This costs time and auxiliary space.Replace the tail call by updates to local bounds and a local rank:The loop invariant says that , , and selecting rank
def selectIterative(k: Int, l: Int, r: Int): Int = {
require(0 <= l && l < r && r <= a.length)
require(0 <= k && k < r - l)
var low = l
var high = r
var rank = k
while (high - low > 1) {
val p = partition(low, high)
val pivotRank = p - low
if (rank == pivotRank) return a(p)
if (rank < pivotRank) high = p
else {
rank -= pivotRank + 1
low = p + 1
}
}
a(low)
}rank in the active segment yields the originally requested order statistic. The original segment's multiset is preserved, and outside it no entries change. The updates are exactly the recursive reductions proved in part (c). The loop variant is ; a non-returning iteration strictly decreases it. A one-entry segment has only rank zero, establishing the final return. Auxiliary space is , rather than a potentially deep call stack.Use the already-filled prefix itself for membership tests. The outer loop invariant is and for . The inner loop invariant says that and no processed entry before
Long intermediates avoid overflow in the candidate calculations, while a checked conversion respects the required output type:def recaman(a: Array[Int]): Unit = {
if (a.length == 0) return
a(0) = 0
var i = 1
while (i < a.length) {
val candidate = a(i - 1).toLong - i.toLong
var j = 0
while (candidate > 0L && j < i && a(j).toLong != candidate) {
j += 1
}
val next =
if (candidate > 0L && j == i) candidate
else a(i - 1).toLong + i.toLong
require(next <= Int.MaxValue.toLong, "Sequence value exceeds Int")
a(i) = next.toInt
i += 1
}
}j equals the positive candidate. Its guard either reaches the end of the prefix, finds the candidate, or immediately rejects a nonpositive candidate. Its loop variant is . This establishes exactly the choice required by the recurrence, so the outer loop invariant is preserved. The outer loop variant is .Extra storage is beyond the supplied result array. Membership scans give an upper bound for output entries. Addition, unlike the subtraction branch, is not required to avoid repeats: at indices and the value occurs twice. The code therefore does not try to enforce global distinctness. If an exact value eventually exceeds
Int, the output interface cannot hold it; the check reports that limitation rather than wrapping the recurrence.For result entries the largest required index is , so the bound in part (a)(iii) permits universe size . Check that the chosen universe can itself be expressed as an array length:The loop invariant is that the result prefix contains exactly and the abstraction function of
def recamanBitmap(a: Array[Int]): Unit = {
val n = a.length
if (n == 0) return
val capacity = n.toLong * (n.toLong - 1L) / 2L + 1L
require(capacity <= Int.MaxValue.toLong, "Bitmap universe too large")
val seen = new BitMapSet(capacity.toInt)
a(0) = 0
seen.add(0)
var i = 1
while (i < n) {
val candidate = a(i - 1).toLong - i.toLong
val next =
if (candidate > 0L && !seen.contains(candidate.toInt)) candidate
else a(i - 1).toLong + i.toLong
a(i) = next.toInt
seen.add(a(i))
i += 1
}
}seen is their set of values. The universe bound ensures that each positive candidate being queried and each actual next value is less than capacity; values are nonnegative. Thus the conversions and the restricted add precondition are justified, rather than merely hoped to succeed. At a repeated addition, add returning false is harmless: the set of previously seen values is still updated correctly. The loop variant is . At return every result entry agrees with the original recurrence.Check entries against their own indices, stopping on the first mismatch:The loop invariant is and for every . The loop variant is . A false guard means either every position has passed or the next position is wrong, so the returned Boolean is true exactly for the identity permutation. Neither the game nor its history is changed. Short-circuit evaluation protects the final indexed comparison.
def isIdentity: Boolean = {
var i = 0
while (i < game.length && game(i) == i) {
i += 1
}
i == game.length
}Allocate a distinct game and copy every destination entry from the corresponding source position:The loop invariant says that the receiver is unchanged and destination positions before
def flip(k: Int): Flip = {
require(1 < k && k <= game.length)
val result = new Flip(game.length)
var i = 0
while (i < game.length) {
val source = if (i < k) k - 1 - i else i
result.game(i) = game(source)
i += 1
}
result.flips = k :: flips
result
}i equal the reversal of the first source entries followed by the untouched suffix. The loop variant is . At exit the copying is complete. Reversal is a bijection on positions, so the destination remains a permutation. The returned object's array is independent of the receiver's array, while the immutable tail of its history list can safely be shared. The source's only supplied constructor randomizes the new array before the copy; that work is redundant but does not affect correctness. An additional private constructor could avoid it without changing the required result.Use breadth-first search with the supplied FIFO queue, taking one edge to mean one permitted prefix reversal:The FIFO queue holds pending paths in nondecreasing history length. Initially it holds only the zero-move path. Removing a path at depth and appending its children at depth preserves that order. The inner loop invariant says that precisely moves of the removed state have been appended; its loop variant is while the guard holds. The first identity state removed therefore has the minimum possible number of moves. A stack-based depth-first search does not generally have that property.
def solve(puzzle: Flip): Flip = {
val pending = scala.collection.mutable.Queue[Flip]()
pending.enqueue(puzzle)
while (!pending.isEmpty) {
val current = pending.dequeue()
if (current.isIdentity) return current
var k = 2L
while (k <= current.game.length.toLong) {
pending.enqueue(current.flip(k.toInt))
k += 1L
}
}
throw new IllegalStateException("No solution")
}
val puzzle = new Flip(n)
println("Solving:")
println(puzzle)
val answer = solve(puzzle)
println("Solved:")
println(answer)Termination does not rely on avoiding repeats in this first version. Every permutation can be sorted by prefix reversal sorting: place the largest misplaced value at the front if necessary, flip it into its final position, and repeat on the shorter prefix. This constructs a route of at most moves. Each search depth has finitely many paths, with at most children per path, so breadth-first search reaches some solution depth after finitely many expansions. This gives a finite bound on remaining expansions before the first solution even though the repeated-state path tree is infinite. The one-element game is already solved. Repeated paths can nevertheless make time and storage enormous; part (e) removes that waste.
Insert before the first entry that is at least the new value; equal values remain separate occurrences:In the scanning branch, the loop invariant says that
class ListPriorityQueue extends PriorityQueue[Int] {
private var first: Node = null
def clear(): Unit = { first = null }
def isEmpty(): Boolean = first == null
def insert(x: Int): Unit = {
if (first == null || x <= first.value) {
first = new Node(x, first)
} else {
var p = first
while (p.next != null && p.next.value < x) {
p = p.next
}
p.next = new Node(x, p.next)
}
}
def delMin(): Int = {
require(first != null, "Empty priority queue")
val result = first.value
first = first.next
result
}
}p is reachable and all values from first through p are strictly smaller than x. The rest of the chain is unchanged and remains sorted. The loop variant is the number of nodes after p. At exit either the next value is at least x or there is no next node, so inserting between p and p.next preserves the representation invariant and adds exactly one occurrence under the abstraction function. The head branch covers an empty chain, a new minimum and equality with the old minimum. delMin returns the head's minimum value and removes exactly that occurrence.Insertion is worst-case;
delMin, isEmpty and the head-resetting clear are . Reclaiming an abandoned chain later is garbage-collection work, not an explicit traversal performed by clear. Storage is , including separate nodes for duplicate values. No fixed insertion-capacity precondition has been added.Use one cached optional result. Only a request for availability or the next result fills that cache:This is a demand-driven filtering iterator. When the cache is empty, its abstract remaining sequence is the filtered remaining input. When it holds
class FilterIterator[T](test: T => Boolean, iter: Iterator[T])
extends Iterator[T] {
private var cached: Option[T] = None
private def prepare(): Unit = {
while (cached.isEmpty && iter.hasNext) {
val x = iter.next()
if (test(x)) cached = Some(x)
}
}
def hasNext: Boolean = {
prepare()
cached.nonEmpty
}
def next(): T = {
prepare()
cached match {
case Some(x) =>
cached = None
x
case None => throw new NoSuchElementException("Filtered iterator exhausted")
}
}
}Some(x), the abstract sequence is x followed by the filtered remaining input. The loop invariant for prepare says that all input elements consumed during the present search have failed test, except for the one cached passing value if one has been found. The first passing value stops the loop, so it cannot read past a result that the client has not yet consumed.Construction performs no underlying reads, and repeated
hasNext calls reuse a cached result. next also works without a preceding hasNext, clears only the result it returns, and does not prefetch its successor. Some(x), rather than Option(x), allows a passing null value to remain a genuine cached value. For finite remaining input, its length is a loop variant; for infinite input, availability can legitimately run forever if no further passing element exists. Deterministic terminating tests and exclusive ownership of the consuming input are assumed. One cache slot is extra storage.Use the remainder form of the Euclidean algorithm to compute the greatest common divisor, then divide both components of the fraction by it:The loop invariant is , , and . Initially it holds by symmetry of the greatest common divisor. For , the integer division identity , with , shows that and have exactly the same common integer divisors. Thus the update preserves the loop invariant. The loop variant is the nonnegative integer , which strictly decreases on each iteration. At exit , so . Dividing by preserves the rational number and makes the returned components coprime. In particular, zero is returned as . No multiplication is needed, and all remainders remain within the original nonnegative
def Reduce(num: Int, den: Int): (Int, Int) = {
require(0 <= num && num < den)
var a = den
var b = num
while (b != 0) {
val r = a % b
a = b
b = r
}
(num / a, den / a)
}Int range.Maintain an accumulated array of denominators and an exact remaining fraction. The usual greedy algorithm can require a denominator larger than The loop invariant is , , all entries of
Int.MaxValue, even for an input with Int components. The following implementation uses arbitrary-precision integers internally. If that representational limit is reached, it returns the always-valid alternative consisting of num copies of . Repeated denominators are permitted by the given Egyptian fraction representation.def fromRat(num: Int, den: Int): Array[Int] = {
require(0 <= num && num < den)
val start = Reduce(num, den)
var n = BigInt(start._1)
var d = BigInt(start._2)
var e = Array.empty[Int]
while (n > 0) {
val q = (d + n - 1) / n
if (!q.isValidInt) return Array.fill(num)(den)
e = e :+ q.toInt
val nextN = n * q - d
val nextD = d * q
val g = nextN.gcd(nextD)
n = nextN / g
d = nextD / g
}
e
}e are positive, andAppending and replacing the residual by preserves this equality; division by the greatest common divisor preserves the residual's value. The loop variant is , by the proof in part (b). If nextN is zero, its greatest common divisor with nextD is nextD, giving residual . On normal exit the residual is zero and the returned array has exactly the required value. On the early-return branch, num copies of have that same value directly; the partial greedy Egyptian fraction expansion is discarded. num=0 returns an empty array.The fallback is a correctness provision for the fixed result type, not an efficiency claim: a large repeated-term array can be impractical. An array of arbitrary-precision integers would retain the greedy Egyptian fraction expansion without this fallback. Allocation, as with any output-producing program, requires enough available memory. The
BigInt remainder, greatest common divisor and checked conversion operations are documented in [ref]Scala 2.12 BigInt API documentation. Methods gcd, isValidInt and toInt
.An Egyptian fraction need not be proper: several positive unit fractions may sum to at least one. Accordingly, accumulate a general nonnegative reduced fraction, rather than calling the proper-input-only The loop invariant is , , , , andWriting , the fraction for the extended prefix has numerator and denominator . These are the
Reduce on every intermediate value. First define an exact helper:def toRatExact(e: Array[Int]): (BigInt, BigInt) = {
var n = BigInt(0)
var d = BigInt(1)
var i = 0
while (i < e.length) {
require(e(i) > 0)
val x = BigInt(e(i))
val g = d.gcd(x)
val nextN = n * (x / g) + d / g
val nextD = d * (x / g)
val h = nextN.gcd(nextD)
n = nextN / h
d = nextD / h
i += 1
}
(n, d)
}
def toRat(e: Array[Int]): (Int, Int) = {
val result = toRatExact(e)
require(result._1.isValidInt && result._2.isValidInt,
"Reduced result does not fit (Int, Int)")
(result._1.toInt, result._2.toInt)
}nextN and nextD in the code. Reducing them preserves the value and restores coprimality. The loop variant is . At exit the helper returns the exact sum in lowest terms, including for the empty array.There are three distinct ways to control integer overflow: cancel the common denominator factor before multiplication, reduce after each addition, and use arbitrary-precision arithmetic when the remaining values still exceed fixed-width bounds. Cancellation reduces intermediate size but cannot guarantee that an exact answer fits
(Int, Int). For example, the sum is in lowest terms, whose denominator exceeds Int.MaxValue. No implementation returning that fixed type can represent every permitted input exactly. The wrapper therefore checks this unavoidable result-type limitation instead of silently truncating; toRatExact supplies the unrestricted mathematical result.[ref]Scala 2.12 BigInt API documentation. Checked representability with isValidInt before the potentially truncating toInt conversion
Print separators before all but the first term, so there is neither a leading nor a trailing plus sign:The loop invariant says that exactly the first unit fractions have been printed in order, separated by
def printRat(num: Int, den: Int): Unit = {
print(num.toString + "/" + den.toString)
}
def printEgypt(e: Array[Int]): Unit = {
if (e.isEmpty) print("0")
var i = 0
while (i < e.length) {
if (i > 0) print(" + ")
print("1/" + e(i).toString)
i += 1
}
} + , with no trailing separator. The loop variant is . The empty array is displayed as zero. Since and , the output is 5/7 = 1/2 + 1/5 + 1/70. The source's earlier example with middle denominator and final denominator contains the arithmetic typo; its final printing example is correct. Indeed , so no positive final term could repair that particular prefix. The printing routine reports the generated terms rather than imposing a particular expansion.