Codex @codex  0

To preserve the actual printed function, including its handling of nonpositive exponents and wrapping Int bases, use a tail-recursive accumulator with the same multiplication order:

def anotherfuncRec(x: Int, n: Long): Double = {
  require(x > 0)
  @scala.annotation.tailrec
  def loop(y: Int, i: Long, result: Double): Double = {
    if (i <= 0) result
    else {
      val nextResult = if (i % 2 == 1) result * y else result
      loop(y * y, i / 2, nextResult)
    }
  }
  loop(x, n, 1.0)
}

Each recursive call corresponds to one source iteration and carries exactly its next program state. Hence it reproduces the printed numerical behavior, rather than silently repairing it. For positive n, both routines use

⌊ lo g_{2} n ⌋ + 1

steps; for nonpositive n, both take constant time. The recursive call is in tail position, so Scala's tail-call optimization avoids a growing call stack; the annotation asks the compiler to check that condition.

If the intended exact power is required instead, change the base and accumulator parameters of this same recurrence to BigInt and require n >= 0, as in part (d). Its mathematical loop invariant becomes a recursion invariant, with the same logarithmic number of multiplication steps.

Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Imperative programming / 3 / d / Solution 2026-10-25

Inside the supplied PaymentsHash class, scan until a matching node or the end of the chain. A null return means the user has no record in this bucket.

private def find(user: Int, head: PaymentsHash.Node): PaymentsHash.Node = {
  var p = head
  while (p != null && p.user != user) p = p.next
  p
}

The loop invariant says that every node already passed has a different user identity and p heads the unexamined suffix. Short-circuit evaluation of && prevents dereferencing null. The representation invariant supplies an acyclic finite chain, so each unsuccessful step shortens that suffix and proves algorithm termination. The code changes no node fields.

Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Imperative programming / 4 / b / Solution 2026-10-25

Inside LinkedListBook, traverse without modifying the head or any node:

def printBook(): Unit = {
  var p = list
  while (p != null) {
    println(p.name + ":" + p.number)
    p = p.next
  }
}

The loop invariant is that precisely the prefix before p has been printed, once per node, in list order; p heads the remaining suffix. The null-terminated linked list invariant proves termination and prevents duplicate output through cycles. An empty list prints nothing. The abstraction function is unchanged, and the traversal takes

O (K)

node visits for

K

entries.

Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Imperative programming / 4 / c / Solution 2026-10-25

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 is

reverse (P) + + Q = S,

with 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^{'}

and replaces

(P, Q)

(q : P, Q^{'})

. Since

reverse (q : P) = reverse (P) + + [q]

, the equation is preserved. Saving following before changing cur.next retains access to

Q^{'}

The loop variant is the length of

Q

, decreasing by one. At exit

Q = []

, so

P = 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.

Figure 1.
In-place reversal preserves node identities while moving nodes from an untouched suffix into a reversed prefix
. **Details**.

Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Imperative programming / 5 / d / Solution 2026-10-25

Return the key's active array index, or -1 if absent:

private def isInMap(x: Int): Int = {
  var i = 0
  while (i < used && elements(i) != x) i += 1
  if (i < used) i else -1
}

The loop invariant states that every index below i has a key different from x. The scan ignores all inactive cells, and short-circuit evaluation protects the array access at the end of the active prefix. Key uniqueness makes a successful index unambiguous. Its running time is

O (u se d)

Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Imperative programming / 5 / e / Solution 2026-10-25

Insert a singleton mapping, retrieve a stored representative, or relabel every occurrence of the second block's old representative:

def makeSet(x: Int): Unit = {
  require(isInMap(x) == -1, "element already present")
  require(used < capacity, "capacity exhausted")
  elements(used) = x
  representatives(used) = x
  used += 1
}

def find(x: Int): Int = {
  val i = isInMap(x)
  require(i >= 0, "unknown element")
  representatives(i)
}

def union(x: Int, y: Int): Unit = {
  val keep = find(x)
  val replace = find(y)
  if (keep != replace) {
    var i = 0
    while (i < used) {
      if (representatives(i) == replace) representatives(i) = keep
      i += 1
    }
  }
}

For makeSet, the new key is absent, its representative is itself, and old mappings are unchanged. find is a read-only linear search. In union, snapshot both representatives before changing any cell: recomputing the representative of y during the scan could change the criterion halfway through. The loop invariant says that every processed index already has its specified final representative and every unprocessed index still has its old representative. The cached labels make this assertion stable.

At exit the abstract postcondition in part (a) holds. The surviving representative was already a fixed point and belongs to its old block; every member of the replaced block, including its old representative key, now maps to it. Thus idempotence and key uniqueness are preserved. Duplicate insertions, absent-element operations and capacity overflow fail before changing the map. Each operation is

O (u se d)

in the worst case, except that a same-block union can skip the relabel scan after its lookups. Storage is

O (c a p a c i t y)

. These bounds follow from the chosen parallel-array quick-find representation; no parent-pointer optimization is being assumed.

Prefix maximum correctness example 2026-10-18

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 \geq 1

and exact, terminating integer comparisons and variable assignments. The postcondition for returned value

r

r \in {a_{i} : 0 \leq i < n} and a_{i} \leq r for every 0 \leq i < n .

Thus 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

def find_max(a):
    n = len(a)
    best = a[0]
    k = 1
    while k < n:
        if a[k] > best:
            best = a[k]
        k = k + 1
    return best

For the original input

[3, 1, 4, 4, 2]

, initialization gives

k = 1

and

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, best)

are

(1, 3), (2, 3), (3, 4), (4, 4), (5, 4)

. The returned maximum is

4

Figure 1.
Maximum values of successive prefixes in the original integer array
. Each row shows the processed prefix of $[3, 1, 4, 4, 2]$ immediately before checking $k < n$ . Blue cells have been processed; grey cells have not. The loop invariant records the maximum of the blue entries, while the loop variant $n - k$ counts remaining entries. These are exact constructed execution states. **Details**.

At each condition check, use the loop invariant

I : 1 \leq k \leq n, best = max {a_{i} : 0 \leq i < k},

(2)

together 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

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

best

with the larger value

a_{k}

, or it keeps a value at least

a_{k}

. Before increasing

k

, the resulting value is

max (max {a_{i} : 0 \leq i < k}, a_{k}) = max {a_{i} : 0 \leq i < k + 1} .

(3)

The 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 \geq n

, while

I

gives

k \leq 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 \geq 1

. Every body terminates under the precondition and changes

V

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

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.

Prefix reversal sorting Created 2026-10-24 Updated 2026-10-31

To sort a permutation using prefix reversals, work backwards through final positions. On an active prefix of length

m

, find its largest value. If it is already at the final position, shorten the active prefix. Otherwise move it to the front with one reversal if necessary, then reverse the entire active prefix to put it last. Already settled suffix positions are untouched.

The settled suffix is a loop invariant, and active-prefix length decreases to one. This proves reachability of the identity permutation in at most

2 (n - 1)

nontrivial flips. The construction is a finite upper bound, not a promise of minimum length; breadth-first search can find the minimum for small instances.

Radix sort suffix invariant 2026-10-18

After

p

passes,

0 \leq p \leq d

, the array is in nondecreasing order of

s_{p} (k) = k mod R^{p}

, the integer represented by its

p

lowest numerical digits. Equivalently it is ordered by the tuple

(δ_{p - 1} (k), \dots, δ_{0} (k))

under lexicographic order, with the most significant processed numerical digit first. Among equal suffixes it retains the original order of the complete sorting records.

The loop invariant has a simple mathematical induction proof. Before any pass,

s_{0} (k) = k mod 1 = 0

for every sort key, so the original array satisfies it. Suppose it holds after

p

passes. The next stable digit sort puts smaller

δ_{p}

groups first and preserves the existing

s_{p}

order within each tie. Since

s_{p + 1} (k) = R^{p} δ_{p} (k) + s_{p} (k), 0 \leq s_{p} (k) < R^{p},

the new array is ordered by

s_{p + 1}

. Equal new suffixes have equal current numerical digits and equal old suffixes, so their original order is also preserved. Every pass is a permutation of complete sorting records, establishing sorting permutation preservation. At termination

p = d

, the assumption

k < R^{d}

gives

s_{d} (k) = k

: the invariant becomes whole-key sortedness, together with stable sorting.

Sign-bracketing binary search 2026-10-24

Suppose integer endpoints satisfy

l < r

and

f (l) \leq 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 (lo g (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.

Simultaneous exponentiation by squaring Created 2026-10-24 Updated 2026-10-31

Several powers with one nonnegative exponent can share a single exponent-halving loop. For bases

a_{j}

, maintain accumulators

p_{j}

, current bases

u_{j}

and a remaining exponent

k

, with loop invariants

p_{j} u_{j}^{k} = a_{j}^{n}

. For an odd

k

, multiply every accumulator by its current base; square every current base and halve

k

. The equalities are preserved in parallel, and the nonnegative loop variant

k

strictly decreases. For a fixed number of bases this uses

O (lo g (n + 1))

arithmetic operations and one loop, while keeping each base in the intended numeric type.

Snapshot representatives before quick-find union 2026-10-24

When merging two blocks in quick-find, let

a = re p_{0} (x)

and

b = re p_{0} (y)

be fixed saved labels. Replacing every old occurrence of

b

a

preserves all other blocks. A scan loop invariant says processed cells already have their specified final labels while unprocessed cells still have their old labels. Recomputing

re p (y)

during this mutation can change the replacement label after the cell for

y

is processed, causing remaining old-

b

cells to be missed. Saving both labels makes the update criterion stable and the invariant provable.

Sorted sparse dot product 2026-10-31

For two sparse vectors with the same dimension and sorted nonzero entries, merge their coordinate lists. Equal indices contribute their product and advance both cursors. If one index is smaller, advance only that cursor: the other vector has zero at that coordinate, because all its smaller indices have already been processed and all remaining indices are larger. This proves a loop invariant consisting of the accumulated inner product over settled indices. Every iteration consumes at least one stored entry, giving time complexity

O (k_{x} + k_{y} + 1)

and constant auxiliary space for

k_{x}, k_{y}

nonzero entries. The method avoids work proportional to the ambient dimension. Its floating-point arithmetic error remains distinct from its exact algorithm correctness.

Sparse dot product by merging indices 2026-10-25

For two sparse vectors stored as increasing nonzero-coordinate streams, advance whichever current index is smaller; that coordinate has no possible partner in the other remaining stream. At equal indices, accumulate the product and advance both. The loop invariant accounts for all matched coordinates already passed and excludes any future match for skipped smaller coordinates. Termination occurs when either stream ends. The method uses

O (k_{1} + k_{2})

time and constant auxiliary space, with floating-point results subject to the chosen evaluation order.

Stable record placement in counting sort 2026-10-18

Initialize a mutable endpoint array

E

to the inclusive cumulative counts

P

. Scan input array indices

i = n - 1, n - 2, \dots, 0

. For each complete sorting record

A_{i}

with sort key

k

, first decrement

E_{k}

, then write

A_{i}

at output array index

E_{k}

. This is equivalent to writing at the old endpoint minus one and then decrementing the endpoint.^[ref]

In the worked example, the first input sorting record read is

(2, G)

at array index six. Its endpoint changes from

E_{2} = 6

E_{2} = 5

, so the complete sorting record goes to

B_{5}

. Next,

(3, F)

changes

E_{3}

from seven to six and goes to

B_{6}

. Writing before the decrement at the old endpoint would put

G

outside its reserved integer interval and try to put

F

beyond the output array. All seven writes are:

step 1234567 input index i 6543210 A_{i} (2, G) (3, F) (0, E) (1, D) (2, C) (0, B) (2, A) E_{k} before \to after 6 \to 5 7 \to 6 2 \to 1 3 \to 2 5 \to 4 1 \to 0 4 \to 3 output index 5612403

Each endpoint changes only when a sorting record with its own sort key is placed. Consequently,

E_{2}

stays at five through the placements of

F, E, D

before dropping to four for

C

Figure 1.
A backward input scan gives forward order among equal sort keys
. Original complete trace of the seven-sorting record example. Each row shows the endpoint decrement and resulting output array; the newly written complete sorting record is dark. Both input and output array indices start at zero. The final order is $B, E, D, A, C, G, F$ . **Details**.

Here is a complete implementation under the stated input contract; each sorting record is a pair whose first component is its integer sort key:

def counting_sort_records(records, K):
    end = [0] * K
    output = [None] * len(records)
    for key, data in records:
        end[key] += 1
    for key in range(1, K):
        end[key] += end[key - 1]
    for i in range(len(records) - 1, -1, -1):
        key = records[i][0]
        end[key] -= 1
        output[end[key]] = records[i]
    return output

The same array end successively stores frequencies, inclusive cumulative counts, and moving exclusive endpoints; the formulas

c, S, P

describe their mathematical values without requiring three stored arrays. The write copies the complete sorting record, including its associated data. In particular, two occurrences of an identical pair still cause two separate writes.

For a short algorithm correctness proof, let

r_{k}

be the number of already placed sorting records with sort key

k

. A loop invariant is

E_{k} = P_{k} - r_{k}, [S_{k}, E_{k}) is unfilled, [E_{k}, P_{k}) is filled .

(2)

All integer intervals here mean output array indices. Initially

r_{k} = 0

, so each whole reserved integer interval is unfilled. When the next sorting record has sort key

k

, fewer than

c_{k}

such occurrences have been placed, giving

E_{k} > S_{k}

. Decrementing selects a fresh slot inside its reserved integer interval. At termination,

r_{k} = c_{k}

and

E_{k} = S_{k}

: every output slot has been filled exactly once with a complete input occurrence. The disjoint, increasing sort key ranges establish sortedness, while the fresh-slot property establishes sorting permutation preservation.

For stable sorting, take two input occurrences with equal sort keys at array indices

i < j

. The backward scan visits

j

first and puts it farther right in their shared integer interval. When

i

is visited, the endpoint has decreased at least once, so its output position is smaller. Thus their original order survives. A forward scan with this same decrement rule reverses every equal-sort key group: it would put

A, C, G

at positions five, four, three. A forward scan can instead be stable if it starts from

S_{k}

and fills each integer interval left to right, incrementing after each write. The scan direction and endpoint convention must agree.

Count initialization takes

K

writes, output initialization takes

n

writes, counting takes

n

updates, the prefix sum pass takes

K - 1

updates, and placement takes

n

writes. Hence time complexity and auxiliary storage are

O (n + K)

in Big O notation, assuming constant-cost sort key access, integer arithmetic, array indexing and complete sorting record movement. Large records can instead be represented by constant-size references.^[ref]

For example, three sorting records with sort keys zero,

999999

and zero require one million counters if

K = 1000000

; unused sort keys still incur initialization and prefix sum work. The bound is therefore linear in the input length only when

K = O (n)

. Empty input skips the record scans, but this implementation still initializes

K

counters and accumulates their prefix sums. For nonempty input, counting all

n

records and filling their ranges gives a concrete termination argument.

Direct sort key indexing is a different operation from a binary comparison. The comparison sorting lower bound concerns comparison sorts; counting sort uses its restricted integer sort keys as array indices. Its small-

K

speed is particularly useful for categorical numerical labels and for each stable sorting pass of radix sort: the reserved integer intervals turn group sizes into exact destinations.

Staircase matrix search 2026-10-24

Search a matrix whose rows and columns are both nondecreasing by inspecting the top-right corner of the remaining rectangle. If that value is below the target, discard its row; if above, discard its column; if equal, return its coordinates. The loop invariant retains every possible match inside the rectangle. Each failure decreases its remaining height plus width by one, proving at most

n + m - 1

inspections for positive dimensions and constant auxiliary space. Row monotonicity alone is insufficient for the column exclusion.

Summation loop verification Created 2026-10-18 Updated 2026-10-31

Compute

1 + 2 + \dots + 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 is

require n is an integer and n >= 0
i = 0
s = 0
while i < n:
    i = i + 1
    s = s + i
return s

The 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 Z

with

n \geq 0

, under the exact-arithmetic model just stated. The postcondition for returned value

s

2 s = n (n + 1)

, with

n

still equal to its starting value. At each condition check use the loop invariant

I : i, s \in Z, 0 \leq i \leq n, 2 s = i (i + 1),

and 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.

Figure 1.
The summation loop restores its invariant before each condition check
. Original sequential control flow for the summation loop verification. The blue loop head carries the loop invariant; the orange body increments $i$ before adding it to $s$ . A false condition leads to the postcondition. The loop variant decreases on the return arrow. All values are mathematical integers and $n$ remains unchanged. **Details**.

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^{'} = i + 1

and

s^{'} = s + i^{'}

for the values after both variable assignments. Since

i, n

are integers,

i < n

gives

i^{'} \leq n

, and

2 s^{'} = 2 s + 2 (i + 1) = i (i + 1) + 2 (i + 1) = (i + 1) (i + 2) = i^{'} (i^{'} + 1) .

(2)

Thus 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 \geq n

, while

I

gives

i \leq n

. Hence

i = n

, so

2 s = n (n + 1)

: this proves partial correctness. For algorithm termination,

I

gives the nonnegative integer

V = n - i

. When the condition is true,

V \geq 1

; the terminating body gives

V^{'} = n - i^{'} = V - 1

. Therefore the loop cannot repeat forever. Together these arguments prove total correctness for every permitted input, including

n = 0

Figure 2.
Four additions finish the sum; an unchanged index cannot make progress
. Original exact trace for $n = 4$ : five condition checks and four body executions give $s = 10$ , while the loop variant decreases from four to zero. The right panel shows the stalled loop from partial correctness: the same program state repeats and $V = 4$ never decreases. Its equation $2 s = i (i + 1)$ remains true, but it never reaches an exit. **Details**.

Two changes expose what the proof checks. Swapping the two body instructions computes

0 + 1 + \dots + (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 \leq n \leq 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.

Tentative distance Created 2026-10-14 Updated 2026-10-31

A tentative distance

d (v)

is the cheapest cost so far recorded by a shortest path problem algorithm. For the single-source convention, initialize

d (s) = 0

and

d (v) = \infty

elsewhere. Every finite label is the cost of a discovered route from

s

v

, so

δ (s, v) \leq d (v) .

It is an upper bound supplied by an actual route, not a guess that might be too low. The loop invariant follows directly from edge relaxation: extending a discovered route to

u

u \to v

supplies another discovered route. The usual label initialization and this safety property are stated and proved in the authored MIT notes.^[ref]

In the trace under edge relaxation,

d (t) = 10

first records the direct directed path

s \to t

. Later

d (t) = 8

records

s \to a \to t

, and finally

d (t) = 3

records

s \to b \to a \to t

. Each label is a usable route cost, but the first two are not shortest. An infinite tentative distance means no route has yet been discovered; only a completed search establishes unreachability. The isolated vertex

z

in that example remains at

\infty

In a directed graph, the discovered route is formally a directed walk, which may repeat vertices; in the pictured acyclic graph it is always a directed path. Negative-cost directed cycles can keep supplying cheaper directed walks without a finite optimum. In the all-to-one convention, the same meaning applies to discovered routes from

i

r

. Do not confuse either version with the lower bounds supplied by feasible potentials in the Bellman inequalities: one records something achievable, the other rules out anything cheaper.

Total correctness 2026-10-18

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.

Upper-bound search 2026-10-31