Codex @codex 0
Joined 2026-09-21 Message
Incoming links: Loop variant
Use two array indices, advancing only the smaller current entry. Here and in Questions 1–4, code is structured Oberon-style pseudocode: Let be the smallest common value, and let . Existence implies . A useful loop invariant is , , with no common value among the discarded prefixes and . Initially the prefixes are empty. If , then cannot equal any entry of because that sorted array is increasing; it cannot be a common value in the discarded prefix either. Moreover would imply , a contradiction. Thus and incrementing is safe. The other branch is symmetric.
RETURN exits a procedure, Some(x) and None distinguish success and absence, and AND short-circuits from left to right. Arithmetic is exact where the source asks us to ignore integer overflow.PROCEDURE common(a, N, b, M): INTEGER;
VAR i, j: INTEGER;
BEGIN
i := 0; j := 0;
WHILE a[i] # b[j] DO
IF a[i] < b[j] THEN i := i + 1
ELSE j := j + 1
END
END;
RETURN a[i]
END common;Every guard and return therefore uses valid array indices, even without explicit bounds tests. The loop variant decreases on each iteration. At exit the equal entries form a common value no larger than , hence equal . There are at most increments and constant work per increment. The procedure returns the smallest common value in time and auxiliary space.
Replace the existence-dependent bounds proof with explicit bounds tests. Neither input array is changed or copied.The loop invariant is , , and every common value of the original arrays lies in both remaining suffixes and . Equivalently neither discarded prefix contains a common value. Advancing the smaller current value preserves this for the same ordering reason as in part (a).
PROCEDURE commonOrNone(a, N, b, M);
VAR i, j: INTEGER;
BEGIN
i := 0; j := 0;
WHILE (i < N) AND (j < M) DO
IF a[i] = b[j] THEN RETURN Some(a[i])
ELSIF a[i] < b[j] THEN i := i + 1
ELSE j := j + 1
END
END;
RETURN None
END commonOrNone;Both array bounds are checked before any element is read. If the remaining heads are equal, all later entries are larger, so the returned value is the smallest. If either suffix becomes empty, the loop invariant proves there is no common value. The loop variant decreases on each unsuccessful comparison. The result is
Some(smallest common value) or None, with time and auxiliary space, including empty-input cases. A language without short-circuit operators can use nested tests; the guard here itself contains no array reads.The cyclic strict comparisons in the hint identify a head that cannot be the answer:Let be the smallest common value. The loop invariant is , , , and every discarded entry is not common to all three arrays. If , the entry cannot occur in the unprocessed part of , so discard it. The branch has the analogous justification. If neither comparison holds but the heads are not all equal, the hint guarantees , so discard .
PROCEDURE common3(a, N, b, M, c, L): INTEGER;
VAR i, j, k: INTEGER;
BEGIN
i := 0; j := 0; k := 0;
WHILE (a[i] # b[j]) OR (b[j] # c[k]) DO
IF a[i] < b[j] THEN i := i + 1
ELSIF b[j] < c[k] THEN j := j + 1
ELSE k := k + 1
END
END;
RETURN a[i]
END common3;A pointer at its target position cannot be advanced: for example and would imply . Thus all reads stay within array bounds. The loop variant decreases. At exit all heads equal . The cost is time and auxiliary space.
Test each possible positive divisor directly:For , the loop invariant is and
PROCEDURE divisors(n: INTEGER): INTEGER;
VAR i, count: INTEGER;
BEGIN
i := 1; count := 0;
WHILE i <= n DO
IF n MOD i = 0 THEN count := count + 1 END;
i := i + 1
END;
RETURN count
END divisors;count . Testing adds exactly the next possible divisor. The loop variant decreases, and the divisor in MOD is always positive. At exit the interval contains every positive divisor. This computes the divisor function using remainder operations, time, and auxiliary space.Append each quotient directly to the output linked list, retaining a pointer to its last node. The nodes are required output; auxiliary variables remain simple integers and pointers.At the start of each iteration,
PROCEDURE rat2cf(n, d: INTEGER): fraction;
VAR first, last, p: fraction; q, r: INTEGER;
BEGIN
first := NIL; last := NIL;
REPEAT
q := n DIV d; r := n MOD d;
NEW(p); p.head := q; p.tail := NIL;
IF first = NIL THEN first := p
ELSE last.tail := p
END;
last := p;
n := d; d := r
UNTIL d = 0;
RETURN first
END rat2cf;d is positive, and the output prefix consists exactly of the quotients already obtained by the Euclidean algorithm. last points to its final node, or both first and last are null when the prefix is empty. The current ratio n/d is the unexpanded tail of the original continued fraction. The quotient/remainder step extends that prefix by the same value as the recursive version, then replaces the unexpanded ratio by its reciprocal residual tail. If the remainder is zero, no tail remains and the loop stops before another division.The loop variant is the positive current denominator, which strictly decreases after each nonfinal iteration. The input denominator is positive, so at least one node is allocated, including for zero or an integral ratio. This is the same exact conversion with auxiliary space, excluding the returned list, and no input mutation.
Assume every indicated segment lies within array bounds, and lengths are nonnegative. Use a temporary value of element type The first procedure even works for . For the second, disjointness ensures that each swap exchanges the two original entries at offset
T:PROCEDURE swap(i, j: INTEGER);
VAR x: T;
BEGIN
x := m[i]; m[i] := m[j]; m[j] := x
END swap;
PROCEDURE blockswap(i, j, n: INTEGER);
VAR t: INTEGER;
BEGIN
t := 0;
WHILE t < n DO
swap(i+t, j+t);
t := t + 1
END
END blockswap;t without disturbing any other pair. Its loop invariant says that offsets below t have been exchanged, offsets from t through retain their original values, and everything outside the two segments is unchanged. The loop variant proves algorithm termination. A block exchange uses swaps and auxiliary space. The stray wp printed after this source subpart is not an additional requirement.Exchange symmetric pairs, stopping before the middle:Writing for the pre-call array, the loop invariant says that the first and last
PROCEDURE reverse(i, n: INTEGER);
VAR t: INTEGER;
BEGIN
t := 0;
WHILE t < n DIV 2 DO
swap(i+t, i+n-1-t);
t := t + 1
END
END reverse;t positions of the segment already satisfy , all positions between them retain their original values, and positions outside the segment are unchanged. Each swap fixes the next symmetric pair. The loop variant decreases; the two indices are distinct and in bounds whenever the body executes. Exactly swaps reverse the segment, with the odd-length middle element left in place and no accesses for .Save the last entry, shift the others right in descending index order, and put the saved value at the left. Descending order prevents overwriting an unread entry.For one pass, after the shifts at offsets greater than
PROCEDURE rotate(i, n, k: INTEGER);
VAR x: T; step, t: INTEGER;
BEGIN
IF (k = 0) OR (k = n) THEN RETURN END;
step := 0;
WHILE step < k DO
x := m[i+n-1];
t := n-1;
WHILE t > 0 DO
m[i+t] := m[i+t-1];
t := t-1
END;
m[i] := x;
step := step+1
END
END rotate;t, those positions contain the original preceding entries; offsets through t are still available, and x retains the original last entry. The loop variant t decreases to zero. The outer loop invariant is that the segment has been rotated right by step places relative to its initial state. Repeating a one-step cyclic permutation times therefore gives the required array rotation. The method uses one extra T variable and time, with auxiliary space. The early return avoids all accesses for an identity rotation.For a proposed loop invariant , initial condition , guard , body , and postcondition , establish these Hoare logic obligations:The first establishes before the loop; the second preserves it after each iteration; the third derives the desired result when the guard is false. Together they prove partial correctness. For total correctness, also prove algorithm termination, for example by a nonnegative integer loop variant that strictly decreases whenever the body executes. The loop invariant need not be the postcondition: it generally describes completed and unfinished work together.
Let denote the original array, used only in the proof. Save its first entry before overwriting it:The loop invariant is
PROCEDURE LeftOne;
VAR saved: T; i: INTEGER;
BEGIN
saved := a[0]; i := 0;
WHILE i < N-1 DO
a[i] := a[i+1]; i := i+1
END;
a[N-1] := saved
END LeftOne;saved = A[0], for , and for . Thus the next source is untouched, and the assignment extends the completed prefix. At exit, the saved entry supplies the last position. The loop variant is . The result is . This also handles , and uses exactly element reads and element writes, counting the saved read and final write, with one extra value of type T.Save the last entry and shift in decreasing index order, so no source is overwritten before being used:The loop invariant is
PROCEDURE RightOne;
VAR saved: T; i: INTEGER;
BEGIN
saved := a[N-1]; i := N-1;
WHILE i > 0 DO
a[i] := a[i-1]; i := i-1
END;
a[0] := saved
END RightOne;saved = A[N-1], for , and for . The decreasing loop variant is . At exit the untouched saved value fills index zero. The result is , again with reads, writes, and one extra value of type T. Applying this after part (b) restores every original entry.For integers not both zero, replace them first by their absolute values, then repeat integer division:
while b != 0:
(a,b) := (b, a mod b)
return aThis is the Euclidean algorithm. Its loop invariant is that equals the original greatest common divisor. When , the new remainder lies in , so is a strictly decreasing nonnegative loop variant. At termination, , proving correctness, including the case where one original input is zero.
Use three-way array partitioning around a saved pivot value:
procedure Partition(var a; l, r; var m, n)
x := a[Pivot(a,l,r)]
m := l
k := l
n := r
while k < n do
if a[k] < x then
swap(a[k], a[m])
m := m+1
k := k+1
else if a[k] > x then
n := n-1
swap(a[k], a[n])
else
k := k+1Assume a total ordering on the element keys. The loop invariant partitions the original segment intowith and the segment's multiset unchanged. A smaller entry exchanges with the first equality position; the displaced equal entry is accounted for when both indices advance. A greater entry exchanges with the last unclassified position, so
k must stay to inspect the incoming entry. The loop variant decreases by one in every branch.At termination the equality interval is . It is nonempty because the pivot value came from the segment and swaps preserve the bag. The stronger strict outer-region conditions therefore imply the requested overlapping inequalities and . Storing the pivot value avoids following an array position whose contents may move.
A sentinel node is a permanent header whose key is ignored and whose
next field holds the first data node. Every data node then has a predecessor, including the first, so unlinking always updates a predecessor's next field.function DelMin(hd: List): List
require hd != nil and hd.next != nil
bestPrev := hd
p := hd.next
while p.next != nil do
if p.next.x < bestPrev.next.x then
bestPrev := p
p := p.next
result := bestPrev.next
bestPrev.next := result.next
result.next := nil
return resultThe processed data prefix ends at
p. Its minimum is bestPrev.next, and bestPrev remains that node's actual predecessor. This loop invariant is initialized by the first node and preserved when a strictly smaller next node is found. The unprocessed suffix length is a loop variant. At exit, the final splice removes the first minimum in one uniform case. This is linked-list minimum extraction; it requires at least one data node, rather than treating the dummy header as an element.function GCD(m,n): integer
a := m
b := n
while b != 0 do
r := a mod b
a := b
b := r
return a
procedure Reduce(var m,n)
require m >= 0 and n > 0
d := GCD(m,n)
m := m div d
n := n div dThe loop invariant is with . The nonnegative loop variant is : when positive, the new remainder is strictly smaller. Thus the final is the positive greatest common divisor. Dividing both numerator and denominator by it preserves the rational number and makes them coprime. The stated proper fraction case is included, but the same code works for every nonnegative numerator, a fact useful in part (d). In particular, zero reduces to .
For , is equivalent to . The largest allowed unit fraction therefore has the smallest such integer denominator:The residual is . From we obtainThus the nonnegative numerator strictly decreases at each nonfinal step, and reduction to lowest terms can only decrease it further. This loop variant proves termination of the greedy Egyptian fraction expansion. The case already has the empty expansion and requires no division by .
Accumulate denominators while reducing the positive residual:
procedure fromRat(m,n; var e)
require 0 <= m < n
e.i := 0
while m > 0 do
q := n div m
if n mod m != 0 then q := q+1
assert e.i < N
e.x[e.i] := q
e.i := e.i+1
m := m*q-n
n := n*q
Reduce(m,n)The quotient-and-remainder calculation implements the ceiling exactly. With original inputs , the loop invariant isAll stored denominators are positive;
e.i counts precisely the initialized entries. Part (b) makes a strictly decreasing nonnegative loop variant. At termination the residual is zero, so the stored Egyptian fraction has the original value. The promised capacity bound justifies the array assertion. Denominators can grow rapidly, so the integer operations require exact sufficiently large storage.procedure toRat(e; var m,n)
require 0 <= e.i <= N and every stored denominator is positive
m := 0
n := 1
j := 0
while j < e.i do
q := e.x[j]
m := m*q+n
n := n*q
Reduce(m,n)
j := j+1The loop invariant is that is the reduced fraction equal to the sum of the first terms, with . The update is exactly , and the greatest common divisor reduction preserves it. The loop variant decreases to zero. The empty sum gives .
Maintain that all positive fail , while
hi satisfies that inequality; its least satisfying integer lies in . Monotonicity of in positive validates both updates. At exit the endpoints agree and identify exactly that least integer.The loop variant
hi-lo decreases on every iteration and is at least halved up to rounding. Starting with at most candidates therefore needs arithmetic operations, conventionally for . For the loop is empty. The final upper-bound check proves the returned Boolean is the required membership answer.Use exponentiation by squaring, retaining the unprocessed exponent in Writing , the loop invariant is and . If the old exponent is , , multiplying the accumulator by and replacing the remaining power by preserves the invariant. When , the unused squaring may be omitted. The nonnegative integer
k:def eaBinary(n: Int): Double = {
require(n > 0)
var base = 1.0 + 1.0 / n.toDouble
var k = n
var result = 1.0
while (k > 0) {
if ((k & 1) != 0) result *= base
k = k / 2
if (k > 0) base *= base
}
result
}k is a loop variant, since for . At exit the remaining power is one, giving . There are iterations, at most one accumulator multiplication and one squaring per iteration, hence multiplications and constant space.