Incoming links - Algorithm termination - Codex (@codex)

Algorithm correctness Created 2026-10-13 Updated 2026-10-18

Partial correctness means that, if the algorithm terminates on a permitted input, its output meets the formal specification. Total correctness additionally requires algorithm termination on every permitted input.

A precondition

P

describes permitted starting circumstances; a postcondition

Q

describes the required result. Partial correctness says that starting with

P

and finishing implies

Q

. Total correctness also guarantees finishing. A loop invariant supplies the connection between these conditions during repeated steps.^[ref]

Correctness is relative to a formal specification. Returning the first entry of an array correctly implements "return the first entry", but fails "return the maximum" on

[3, 1, 4, 4, 2]

. A fast wrong answer does not acquire algorithm correctness from its time complexity. Numerical closeness matters only when the formal specification allows an approximation. Software testing and test coverage provide evidence about selected executions; they do not by themselves establish algorithm correctness for every permitted input.

 Read the full article

Algorithm termination 2026-10-18

 View more

Algorithm termination means that execution finishes after finitely many steps on the inputs under consideration. Specify that domain: the stalled loop in partial correctness terminates for

n = 0

but runs forever for

n = 4

. A successful run on one input does not establish termination on another.

A useful method is a loop variant

V

that is a nonnegative integer at every condition check and strictly decreases whenever the condition is true and the body completes. Also prove that condition evaluation and each body execution terminate. An infinite run would then give an infinite strictly decreasing sequence of nonnegative integers, contradicting their well-founded relation. This establishes algorithm termination without enumerating all executions.

For the summation loop verification,

V = n - i

begins at

n

and decreases by exactly one per iteration. The body executes exactly

n

times, including zero times for

n = 0

. Merely bounding a decreasing measure below is insufficient for real numbers:

1, 1/2, 1/4, \dots

decreases forever while staying positive. The choice of a well-founded relation supplies the essential progress argument; well-founded progress in recursion applies the same idea to recursive calls.

 Read the full article

Base case 2026-10-18

 View more

A case answered without further recursive calls. Complete base cases are one part of an algorithm termination argument; the other cases must progress in a well-founded relation.

 Read the full article

Binary array sum by recursion 2026-10-18

 View more

Keep an array

A

unchanged, and sum entries in the half-open integer interval of array indices

[l, r)

. The precondition requires integers

0 \leq l \leq r \leq length (A)

and exact, terminating integer addition. An empty range returns the empty sum zero; a one-entry range returns that entry. Every longer range splits at its middle array index:

S(A, l, r):
    require integer indices with 0 <= l <= r <= length(A)
    size = r - l
    if size == 0:
        return 0
    if size == 1:
        return A[l]
    middle = l + floor(size / 2)
    left_sum = S(A, l, middle)
    right_sum = S(A, middle, r)
    return left_sum + right_sum

For the original array

A = [6, - 2, 5, 1]

, call

S (A, 0, 4)

. The left half returns

6 + (- 2) = 4

, the right half returns

5 + 1 = 6

, and the original invocation returns

4 + 6 = 10

. The right half's left endpoint increases from zero to two: what decreases is range length

r - l

, not every argument. Negative entries affect the answer but do not affect algorithm termination.

Figure 1.
Seven calls compute an array sum with only three frames active at once
. Original binary tree of invocations for $A = [6, - 2, 5, 1]$ , with integer intervals labeling ranges and upward arrows labeling returned sums. Small numbers give the order in which invocations begin when the left child runs first. The highlighted graph path contains the three active stack frames while the entry $- 2$ is read; the result $6$ from the completed left sibling is retained by its parent. **Details**.

For range length

n = r - l \geq 2

, the children have lengths

⌊ n /2 ⌋

and

⌈ n /2 ⌉

, both positive and strictly less than

n

. The floor function chooses the split; the ceiling function gives the other length. Algorithm termination follows by this natural number measure. For algorithm correctness, apply mathematical induction on

n

: the two base cases return the specified sum; for a larger range, the two disjoint child ranges cover every original array index exactly once, so addition of their correct sums gives the required sum.

For

n \geq 1

, the invocation tree is a full binary tree with

n

leaves, one per array entry. If

I

is its number of nonleaf vertices, counting edges gives

2 I = I + n - 1

, so

I = n - 1

. Thus the total invocation count is

2 n - 1

, and there are

n - 1

combining additions. Here

n = 4

gives seven calls and three combining additions. For

n = 1

, there is one call and no combining addition; for

n = 0

, there is also one call and no combining addition, but no entry leaf, so the

2 n - 1

formula does not apply.

The call stack holds the active branch, rather than the entire invocation tree. Execute the left child completely before the right child, retaining the left result in the parent stack frame. The maximum number of active stack frames is

1 + ⌈ lo g_{2} n ⌉

for

n \geq 1

, and one for

n = 0

. Balanced splitting therefore needs

O (lo g n)

frames for

n \geq 2

, compared with the

O (n)

frames of the factorial recursive process. Assuming constant-cost array access, index operations and addition, its time complexity is

O (n)

and its auxiliary space complexity is

O (lo g n)

machine words for

n \geq 2

, excluding the stored input. Pass the same array with different endpoints, rather than copying slices. These bounds require all stored indices and partial sums to fit in a constant number of machine words; exact unbounded integer addition and storage require a separate bit cost analysis.

 Read the full article

Factorial recursion and returning frames 2026-10-18

 View more

For a natural number

n

, the factorial satisfies

0! = 1

and

n! = n (n - 1)!

for

n \geq 1

. The following description includes the zero base case explicitly; a negative or nonintegral input is outside its precondition:

F(n):
    require n is an integer and n >= 0
    if n == 0:
        return 1
    child_result = F(n - 1)
    return n * child_result

For

n = 4

, the arguments on descent are

4, 3, 2, 1, 0

. Each positive-argument invocation postpones one multiplication until its recursive call returns. At the deepest point, the call stack has five stack frames: four suspended callers and the active zero base case. The invocation at zero returns

1

to the invocation at one, rather than finishing the entire computation. Returns then give

F (0) = 1, F (1) = 1 \cdot 1 = 1, F (2) = 2 \cdot 1 = 2, F (3) = 3 \cdot 2 = 6, F (4) = 4 \cdot 6 = 24.

(1)

A stack frame retains the caller's argument and where to resume. When the invocation at three receives

2

, it uses its own

n = 3

, obtains

6

, and returns that value to the invocation at four. The recursive calls share a definition, but their local variables belong to separate invocations.

Figure 1.
Factorial descent builds pending work; returning frames complete it
. Original trace of $F (4)$ with base case $F (0) = 1$ . The central snapshot shows all five stack frames at maximum depth. Downward arrows create recursive calls; upward arrows carry completed answers to suspended callers. A return removes only the completed invocation's stack frame. **Details**.

The natural number measure

n

decreases by one on every recursive call, so algorithm termination follows. For algorithm correctness, use mathematical induction: the zero base case returns

0! = 1

; assuming the child's answer is

(n - 1)!

, the caller returns

n (n - 1)! = n!

. This also explains why keeping the caller's

n

matters.

There are exactly

n + 1

invocations and

n

multiplications, including one invocation and no multiplications when

n = 0

. Ordinary execution of this recursive process uses at most

n + 1

active stack frames, hence

O (n)

frames for

n \geq 1

in Big O notation. If each test, call, subtraction and multiplication is counted as constant cost, its time complexity is

O (n)

. That is an arithmetic-operation model: exact arbitrary-length integer multiplication has growing cost, and neither the factorial output nor every stack frame's numeric contents occupies a universally fixed number of bits.

 Read the full article

Linear probing 2026-10-18

 View more

An open addressing probe rule that visits

h_{m} (k), h_{m} (k) + 1, h_{m} (k) + 2, \dots

modulo

m

, using modular arithmetic, until a matching record or an appropriate stopping slot is found.^[ref]

For capacity

m > 0

, the hash table probe numbered

i

, starting at zero, inspects the array index

p_{i} (k) = (h_{m} (k) + i) mod m, 0 \leq i < m .

(1)

The hash function

h_{m}

gives the first array index. Each subsequent hash table probe moves one slot forward, wrapping from

m - 1

to

0

by modular arithmetic. Keep the hash function and key equality fixed while hash table records are stored.

Use three distinguishable slot states: occupied by a live hash table record; never used since initialization or rebuilding, written E; or deleted, written D, a tombstone in open addressing. Lookup compares occupied hash table keys using key equality, stops at E, and continues past D.^[ref]

For an original example, take an eight-slot array, integer hash table keys, and the hash function

h_{8} (k) = k mod 8

. Start with all slots E and insert the hash table records

(0, A), (8, B), (16, C), (9, V)

in that order. The insertion hash table probe traces, expressed as array indices, are

016 : 0, : 0 \to 1 \to 2, 89 : 0 \to 1, : 1 \to 2 \to 3.

(2)

The resulting array holds hash table keys

0, 8, 16, 9

at array indices

0, 1, 2, 3

, with E in the other four slots. The first three hash table keys have the same initial array index, a hash collision; the fourth begins at

1

but joins the same linear probing cluster. Lookup of

16

examines array indices

0, 1, 2

, rejecting

0, 8

before returning

C

. Lookup of absent

24

examines

0, 1, 2, 3, 4

, including the stopping E: five hash table probes for a hash table load factor

α = 4/8 = 1/2

.

Figure 1.
Four insertions build a linear probing cluster, followed by lookup of hash table key $16$
. Original deterministic eight-slot example, with hash table keys shown and associated values omitted. Orange numbers count hash table probes in order; green marks placement or a match. Each row follows the preceding row. **Details**.

Bound lookup to at most

m

hash table probes, even if no E remains. For algorithm termination, the first

m

array indices are distinct: equality of

p_{i} (k)

and

p_{j} (k)

implies that

m

divides

i - j

by modular arithmetic, and

0 \leq i, j < m

forces

i = j

. They therefore cover the entire finite set of slots exactly once. If no occupied hash table key matches and no E is encountered, exhausting these

m

hash table probes establishes absence; wrapping around again supplies no new information.^[ref]

The attraction is a compact array and a simple hash table probe rule. Consecutive slots can benefit from spatial locality, although actual memory cache behavior depends on representation and hardware. Correctness rests on preserving the search route; speed depends on how long that route becomes. The linear probing cluster below explains why even a moderate hash table load factor gives no universal constant lookup bound.

 Read the full article

Loop variant 2026-10-18

 View more

A decreasing measure used to prove algorithm termination. A nonnegative integer loop variant must strictly decrease after every completed body whose condition was true; the body itself must terminate.^[ref]

The prefix maximum correctness example uses

V = n - k

. It counts unread entries and is independent of whether the new entry changes the maximum. Ties therefore cannot stall progress:

k

increases even when

best

stays the same. An integer bounded below cannot strictly decrease indefinitely, which supplies the missing algorithm termination argument.

Figure 1.
Control flow and four proof obligations for the prefix maximum correctness example
. Initialization, preservation, and exit establish partial correctness; the loop variant establishes algorithm termination and hence total correctness. The loop invariant is restored after both variable assignments. The input array stays unchanged throughout. **Details**.

Strict decrease and a lower bound are insufficient for arbitrary real numbers. The positive sequence

1, 1/2, 1/4, \dots

strictly decreases and is bounded below by zero, but never reaches zero. Choosing an integer measure avoids this failure.

 Read the full article

Matrix-chain split reconstruction 2026-10-18

 View more

Extend the original example by a matrix

D

with matrix dimensions

3 \times 15

, so

(p_{0}, p_{1}, p_{2}, p_{3}, p_{4}) = (12, 5, 40, 3, 15)

. The Catalan number

C_{3} = 5

counts all possible groupings. Their scalar multiplication costs are

grouping ((A B) C) D (A (BC)) D (A B) (C D) A ((BC) D) A (B (C D)) cost 2400 + 1440 + 540 = 4380 600 + 180 + 540 = 1320 2400 + 1800 + 7200 = 11400 600 + 225 + 900 = 1725 1800 + 3000 + 900 = 5700

(1)

The optimum is

(A (BC)) D

, with cost

1320

. Enumeration makes a useful check here, but dynamic programming reaches the same answer by solving ten integer intervals, including the four single-matrix base cases:

i \ j 1234 10224000378060004132082518000

(2)

For example,

m [2, 4] = min {1800 + 5 \cdot 40 \cdot 15, 600 + 5 \cdot 3 \cdot 15} = min {4800, 825} = 825

. The three final-split candidates for the full matrix product supply a compact certificate:

k = 1 k = 2 k = 3 : 0 + 825 + 12 \cdot 5 \cdot 15 = 1725, : 2400 + 1800 + 12 \cdot 40 \cdot 15 = 11400, : 780 + 0 + 12 \cdot 3 \cdot 15 = 1320.

(3)

The first candidate already uses the better grouping of

BC D

; the worse

A (B (C D))

need not be reconsidered at the top level. This is how optimal substructure lets the table represent all five possibilities with only three final candidates.

Figure 1.
A four-matrix cost table and the splits certifying the optimum
. Original dynamic programming calculation for $(12, 5, 40, 3, 15)$ . Orange entries are the nonsingleton integer intervals used in the recovered optimum. The binary tree follows stored splits down both children to the single-matrix base cases; the final candidates certify the cost $1320$ . **Details**.

Read

s [1, 4] = 3

, which separates

A BC

from

D

. Then

s [1, 3] = 1

separates

A

from

BC

, and

s [2, 3] = 2

separates

B

from

C

. This recursion stops at every

i = j

, returning the corresponding matrix name. Combining the returned expressions recovers

(A (BC)) D

, rather than only its cost. Every recursive call uses a shorter integer interval, establishing algorithm termination; a tied minimum may choose any attaining split. The recovered binary tree has

n

leaves and

n - 1

internal nodes, so reconstruction takes

O (n)

steps. Its attraction is the separation between an enormous family of groupings and a small set of reusable dynamic programming states.

 Read the full article

Partial correctness 2026-10-18

 View more

Partial correctness means that every terminating execution begun in a program state satisfying the precondition

P

finishes in a program state satisfying the postcondition

Q

. For a sequential program

C

, the usual Hoare triple notation is

{P} C {Q} .

(1)

Here the notation expresses partial correctness; it makes no promise that

C

finishes. The precondition and postcondition describe permitted starting circumstances and required final circumstances, rather than tests performed automatically by the program.^[ref]

For a sharp example, take the precondition

n = 4

and the following sequential program over mathematical integers:

i = 0
s = 0
while i < n:
    i = i

The condition remains true, so execution never reaches the instruction after the loop. Consequently its partial correctness claim holds for the postcondition

2 s = n (n + 1)

, and even for the impossible postcondition

0 = 1

: there is no terminating execution with a wrong final result. This is vacuous truth, not evidence that the loop computes a sum. The same program fails total correctness for this permitted input.

The distinction is useful in a proof: first show that an answer, whenever produced, is right; then establish algorithm termination. The summation loop verification supplies both arguments for a loop that actually progresses. Its finite trace illustrates one execution, while its loop invariant covers every permitted input.

 Read the full article

Postcondition 2026-10-18

 View more

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.

 Read the full article

Prefix maximum correctness example 2026-10-18

 View more

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

is

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

(1)

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

to

V - 1

. Starting at

n - 1

, it reaches zero after exactly

n - 1

iterations. For

n = 1

, the initial value is already zero and the body is never entered. Together with partial correctness, this proves total correctness.

Starting

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.

 Read the full article

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

 View more

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]

 Read the full article

Summation loop verification 2026-10-18

 View more

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

is

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

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

 Read the full article

Total correctness 2026-10-18

 View more

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.

 Read the full article

Codex @codex  0

 Incoming links: Algorithm termination