Codex @codex  0

Assume every indicated segment lies within array bounds, and lengths are nonnegative. Use a temporary value of element type 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;

The first procedure even works for

i = j

. For the second, disjointness ensures that each swap exchanges the two original entries at offset t without disturbing any other pair. Its loop invariant says that offsets below t have been exchanged, offsets from t through

n - 1

retain their original values, and everything outside the two segments is unchanged. The loop variant

n - t

proves algorithm termination. A block exchange uses $n$ swaps and $O (1)$ auxiliary space. The stray wp printed after this source subpart is not an additional requirement.

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

Let

a = n - k

and

b = k

be the lengths of the left and right blocks. Exchange the smaller block with the equally long block at the opposite end.

PROCEDURE rotate(i, n, k: INTEGER);
VAR a, b: INTEGER;
BEGIN
  IF (k = 0) OR (k = n) THEN RETURN END;
  a := n-k; b := k;
  IF a = b THEN
    blockswap(i, i+a, a)
  ELSIF a < b THEN
    blockswap(i, i+b, a);
    rotate(i, b, b-a)
  ELSE
    blockswap(i, i+a, b);
    rotate(i+b, a, b)
  END
END rotate;

a < b

, split

B = B_{1} B_{2}

with

∣ B_{2} ∣ = a

. The first block swap sends

A B_{1} B_{2}

B_{2} B_{1} A

;

A

is now in its final suffix. Rotate the remaining prefix of length

b

right by

b - a

to send

B_{2} B_{1}

B_{1} B_{2}

. If

a > b

, split

A = A_{1} A_{2}

with

∣ A_{1} ∣ = b

. The swap sends

A_{1} A_{2} B

B A_{2} A_{1}

; the fixed prefix is

B

, and rotating the remaining length-

a

suffix right by

b

restores

A_{1} A_{2}

. In both cases the exchanged segments are disjoint.

The remaining length strictly decreases, so induction on

n

proves algorithm termination and correctness. This implements the block-exchange rotation. It uses only simple explicit variables, but its recursive call stack can have

Θ (n)

depth when one block has length

1

; the iterative version removes that extra storage.

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Imperative programming (resit) / 1 / b / Solution 2026-10-31

Keep both the exponent and its power. This Oberon procedure uses only the permitted arithmetic:

PROCEDURE IntLog(b, n: INTEGER): INTEGER;
VAR i, p: INTEGER;
BEGIN
  i := 0; p := 1;
  WHILE p*b <= n DO
    p := p*b; i := i+1
  END;
  RETURN i
END IntLog;

The loop invariant is

i \geq 0

and

p = b^{i} \leq n

. It holds initially because

n > 0

. A successful guard permits the next power, and the two assignments preserve the relation between

p

and

i

. At exit,

p \leq n < p b

, which is exactly part (a). Each iteration increases

i

, and only finitely many powers of

b \geq 2

are at most

n

, proving algorithm termination. The returned value is $⌊ lo g_{b} n ⌋$ . Its running time is

Θ (1 + lo g_{b} n)

arithmetic operations; integer overflow is deferred to part (e).

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Imperative programming (resit) / 2 / a / Solution 2026-10-31

Separate integer partitions according to whether they contain a part equal to

i

. Removing one such part is a bijection to partitions of

n - i

whose parts are at most

i

. The alternatives are disjoint, giving

p (i, n) = p (i - 1, n) + p (i, n - i) (i \geq 1, n \geq 1) .

Use

p (i, 0) = 1

, because the empty integer partition is counted once, and

p (0, n) = 0

for

n > 0

, with

p (i, n) = 0

for

n < 0

. This Oberon implementation avoids negative recursive arguments:

PROCEDURE P(i, n: INTEGER): INTEGER;
VAR answer: INTEGER;
BEGIN
  IF n = 0 THEN answer := 1
  ELSIF i = 0 THEN answer := 0
  ELSIF i > n THEN answer := P(i-1, n)
  ELSE answer := P(i-1, n) + P(i, n-i)
  END;
  RETURN answer
END P;

PROCEDURE Partitions(n: INTEGER): INTEGER;
BEGIN
  RETURN P(n, n)
END Partitions;

The precondition is

i, n \geq 0

. Each recursive call reduces

i + n

, proving algorithm termination. Every positive part of a partition of

n

is at most

n

, so the required one-argument count is $P (n, n)$ . Counts require a sufficiently wide integer representation.

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Imperative programming (resit) / 4 / a / Solution 2026-10-31

For a proposed loop invariant

I

, initial condition

P

, guard

B

, body

S

, and postcondition

Q

, establish these Hoare logic obligations:

P \Rightarrow I, {I \land B} S {I}, I \land \neg B \Rightarrow Q .

The first establishes

I

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.

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Imperative programming / 5 / c / Solution 2026-10-31

Return the new root of the affected subtree, assigning that result back to the parent's child reference:

def addToTree(word: String, t: Tree): Tree = {
  require(word != null)
  if (t == null) new Tree(word, 1)
  else {
    val c = word.compareTo(t.word)
    if (c < 0) t.left = addToTree(word, t.left)
    else if (c > 0) t.right = addToTree(word, t.right)
    else {
      require(t.count < Int.MaxValue)
      t.count += 1
    }
    t
  }
}
// Updating the whole structure uses: root = addToTree(word, root)

Assume the input binary search tree satisfies part (b)'s representation invariant and, if the key already occurs, its count can be incremented. Structural induction proves the postcondition. For an empty subtree, the fresh entry represents one occurrence. Otherwise the word comparison identifies the only possible child subtree containing the word. The recursive call adds exactly one occurrence there, preserving the inherited strict bounds; in the equal case only the count changes. The number of entries in the current subtree strictly decreases in each recursive call, proving algorithm termination. The returned binary search tree represents the old multiset plus one occurrence of word. With height

h

, at most

h + 1

comparisons are made; without balancing this can be linear in the number of words. Actual comparison work also depends on the compared string data type lengths.

Past exam of the year 1 of the computer science course of the University of Oxford / 2021 / Functional programming, design and analysis of algorithms (resit) / 2 / f / Solution 2026-10-25

An unfold expands a seed into either no node or a bucket and two new seeds:

unfoldTree :: (s -> Maybe (s,[a],s)) -> s -> Tree a
unfoldTree split seed =
  case split seed of
    Nothing -> Empty
    Just (left,equal,right) ->
      Node (unfoldTree split left) equal (unfoldTree split right)

toTreeUnfold :: Ord a => [a] -> Tree a
toTreeUnfold = unfoldTree split
  where
    split [] = Nothing
    split (pivot:xs) =
      let (lo,eq,hi) = partition3 pivot xs
      in Just (lo,pivot:eq,hi)

The seed is the remaining list. Expanding a nonempty seed partitions it exactly as toTree does, and both child seeds are shorter. Induction establishes toTreeUnfold = toTree and algorithm termination on finite inputs. The unfold separates the local decomposition rule from the recursive construction of the tree.

Past exam of the year 1 of the computer science course of the University of Oxford / 2021 / Functional programming, design and analysis of algorithms (resit) / 4 / a / Solution 2026-10-25

A function returning an optional value supplies the representation:

newtype List a = List (Int -> Maybe a)

For a finite represented list, require a length

m \geq 0

such that every index

0 \leq i < m

returns Just its element and every other index returns Nothing. Thus there are no holes: absence at a nonnegative index implies absence at every later index. The type alone does not enforce this invariant, or algorithm termination of a query. An infinite represented sequence may instead have a present value at every nonnegative index; operations requiring its length will not terminate.

The implementations below return Nothing at negative indices. Finite lengths, requested counts and intermediate indices are assumed to fit Int; explicit guards on index shifts also prevent arithmetic wraparound from exposing an invalid element.

Past exam of the year 1 of the computer science course of the University of Oxford / 2021 / Functional programming, design and analysis of algorithms (resit) / 4 / g / Solution 2026-10-25

Merge by comparing the present heads and consuming just the chosen one. The implementation uses only the functional representation:

merge' :: Ord a => List a -> List a -> List a
merge' left right
  | null' left  = right
  | null' right = left
  | head' left <= head' right =
      cons' (head' left) (merge' (tail' left) right)
  | otherwise =
      cons' (head' right) (merge' left (tail' right))

mergeSort' :: Ord a => List a -> List a
mergeSort' input =
  let n = length' input
      middle = n `div` 2
  in if n <= 1 then input
     else merge' (mergeSort' (take' middle input))
                 (mergeSort' (drop' middle input))

The two recursive inputs are the disjoint initial and final portions of the represented sequence; they preserve every occurrence and have smaller lengths when

n \geq 2

. In merge', the smaller current head can precede every remaining value in both sorted inputs. Selecting the left head on equality preserves stability. Each merge step reduces the total number of remaining elements, and induction proves a sorted permutation of the original sequence.

This establishes algorithm termination and correctness on total finite representations, not an unconditional

O (n lo g n)

implementation bound. Nested index functions can make queries costly, and repeatedly finding lengths or heads may revisit them. The familiar merge-sort bound assumes suitable constant-time access or consumption primitives; the source's function-only representation supplies no such cost guarantee.

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Digital systems, linear algebra, introduction to formal proof / 2 / a / Solution 2026-10-25

Use the AAPCS32 convention: r0 holds the input address, r1 the length, and r0 receives the result. The following Thumb instruction set assembly language uses only scratch processor registers, so no callee-saved registers need saving. Assume the array is valid, halfword-aligned, and has nonnegative length; for the mathematical sum assume it fits a signed 32-bit two's complement integer.

.syntax unified
.thumb
.thumb_func
sum16:
    movs r2, #0             @ accumulated sum
    cmp  r1, #0
    ble  .Ldone             @ empty array; also returns 0 if n < 0
.Lloop:
    movs r3, #0             @ Thumb signed load needs a register offset
    ldrsh r3, [r0, r3]      @ signed halfword at a; offset read before r3 changes
    adds r2, r2, r3         @ include this signed value
    adds r0, r0, #2         @ advance by one short, not one byte
    subs r1, r1, #1         @ one fewer element remains
    bne  .Lloop
.Ldone:
    movs r0, r2             @ result register
    bx   lr                 @ leaf routine: lr was not overwritten

After

j

iterations, the loop invariant is that r2 contains the first

j

elements' sum, r0 points to element

j

, and r1 is

n - j

. The sign extension in ldrsh supplies the correct signed addend. One iteration preserves this loop invariant, and the decreasing remaining length proves algorithm termination. For the seven-element calls, the sum lies between

- 229376

and

229369

, so it fits. For longer arrays that overflow, these instructions compute the sum modulo

2^{32}

; that is not a claim about defined signed C programming language overflow behavior. The operand forms are those of the paper's reference sheet.^[ref]

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

A loop invariant is a property of the program state that holds whenever control reaches the loop's condition, including the final failed test. Its main purpose is proving partial correctness: establish it initially, prove one guarded iteration preserves it, then combine it with the negated condition to obtain the postcondition. A separate loop variant or another progress argument proves algorithm termination and hence total correctness.

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

Under exact integer arithmetic, the intended result is $⌈ lo g_{2} x ⌉$ , using the ceiling function. A sufficient loop invariant is

i \geq 0, y = 2^{i}, i = 0 \lor 2^{i - 1} < x .

Initially

i = 0, y = 1

, and the final disjunction is true. If the guard holds, the old value

y = 2^{i}

is below

x

. Incrementing i and doubling y therefore preserves

y = 2^{i}

and makes the new lower bound

2^{i - 1} < x

true. At exit

y \geq x

. If

i = 0

, positivity of

x

forces

x = 1

; otherwise

2^{i - 1} < x \leq 2^{i}

. Both cases establish the claimed postcondition. Doubling eventually reaches or exceeds any fixed positive

x

, proving algorithm termination in this arithmetic model. This is the doubling-loop ceiling logarithm argument.

The printed Scala implementation is not correct for its entire stated Int domain. Its y is an Int. For

x > 2^{30}

, it reaches

y = 2^{30}

, wraps to

- 2^{31}

on the next doubling, then becomes zero and stays zero. The guard remains true forever. The loop invariant above is valid for the printed code only when

1 \leq x \leq 2^{30}

. Scala documents Int as a signed 32-bit value equivalent to Java's primitive int.^[ref]

A corrected implementation for every positive Int input widens the doubling variable before any multiplication:

def ceilingLog2(x: Int): Int = {
  require(x > 0)
  var i = 0
  var y = 1L
  while (y < x.toLong) {
    i += 1
    y *= 2L
  }
  i
}

Now at most 31 iterations are needed and

y \leq 2^{31}

, safely within Long. The same loop invariant proves total correctness without the overflow gap.

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.

Postcondition 2026-10-18

The condition required of a final program state when a program finishes under its precondition. The summation loop verification requires returned value

s

to satisfy

2 s = n (n + 1)

and preserves the input

n

. Relating the answer to the original input matters: allowing the program to replace

n

by zero would change the intended contract.

A postcondition alone gives no promise of algorithm termination. It also need not specify a unique output:

s \geq 0

allows many answers, while the exact triangular number equation determines one integer answer for each permitted

n

. Stronger postconditions express more obligations; proving only a weaker consequence cannot justify the stronger requirement.

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.

Quickselect Created 2026-10-24 Updated 2026-10-31

A selection algorithm that uses array partitioning around a pivot and recursively searches only the side containing the desired order statistic. If there are

s

entries before the placed pivot, an earlier rank is unchanged and a later rank is reduced by

s + 1

. Segment length strictly decreases, proving algorithm termination. The same reduction can update local bounds in a loop, using constant auxiliary space.

Balanced reductions give linear work by a geometric series, while repeatedly discarding only a constant number of entries can give quadratic work. For distinct entries and independent uniform random pivots, a pivot in the middle half has probability at least one half and reduces the retained length to at most three quarters, up to rounding. The expected number of attempts for each such reduction is bounded, so summing expected work over geometric size scales gives

O (n)

expected time. This random-pivot guarantee is not a worst-case guarantee for a deterministic median-of-three heuristic. With duplicates and a strict two-way partition, random pivot choice alone can also fail to shrink an all-equal segment; a three-way partition treats equal keys together.

Recursion (computer science) Created 2026-10-13 Updated 2026-10-18

Recursion solves a problem by invoking the same procedure on smaller instances, with base cases answered directly. For merge sort, an empty or one-entry array is already sorted, and every larger array is split into two shorter parts. The decreasing lengths justify termination; a self-call without a progress rule would not suffice.

A recursive procedure refers to itself, directly or through another procedure. A recursive call starts another invocation, with its own arguments and local variables; the caller can wait for its returned output. A base case supplies an answer without further recursive calls. To establish algorithm termination, also show that every recursive call progresses in a well-founded relation. “Smaller” means smaller in that chosen relation: argument values need not all decrease, and the arguments need not even be numbers.

Recursion is especially expressive when a data structure already decomposes into smaller structures. A binary tree has two child subtrees, so structural recursion can follow its shape. A short rule for each case can describe an entire traversal or computation. The distinction between a recursive procedure and the recursive process it generates helps connect that compact description to its resource use.^[ref]

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.

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.

While loop 2026-10-24

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.