Correctness Reasoning: Preconditions, Postconditions, and Invariants

Reasoning About Correctness Without Running Code

Correctness reasoning is the discipline of proving (on paper) that an algorithm meets its specification for all allowed inputs. Instead of testing many examples and hoping nothing was missed, you make explicit logical claims about the algorithm and verify them step by step.

A practical structure for this kind of proof uses three ingredients:

• Preconditions: what must be true before the algorithm starts (assumptions about inputs and initial state).
• Postconditions: what must be true when the algorithm finishes (the goal, stated precisely).
• Invariants: statements that remain true at key points during execution (especially at the start/end of each loop iteration).

When these are written clearly, you can verify correctness by checking that: (1) the precondition is enough to start safely, (2) the invariant is initially true, (3) each loop iteration preserves the invariant, and (4) when the loop ends, the invariant plus the loop-exit condition implies the postcondition.

Preconditions: What You Are Allowed to Assume

A precondition is not something the algorithm “makes true”; it is something the caller must guarantee. If the precondition is violated, the algorithm is not required to behave correctly.

Examples of preconditions:

Continue in our app.

You can listen to the audiobook with the screen off, receive a free certificate for this course, and also have access to 5,000 other free online courses.

Or continue reading below...

Download the app

• n is an integer and n >= 0.
• arr is a list of numbers with length len(arr) > 0.
• low and high are valid indices and 0 <= low <= high < len(arr).

Good preconditions are minimal (don’t assume more than needed) and explicit (no hidden assumptions like “the list is sorted” unless you state it).

Postconditions: The Contract You Must Deliver

A postcondition describes the required final state. It should be checkable and unambiguous.

Examples of postconditions:

• “Returns the maximum value in arr.”
• “Returns an index i such that arr[i] == target, or returns -1 if no such index exists.”
• “After completion, arr is sorted in nondecreasing order and is a permutation of the original elements.”

Notice that some postconditions include both a value requirement and a structural requirement (e.g., sortedness plus permutation).

Invariants: What Stays True While the Loop Runs

An invariant is a statement that is true at a specific repeated point in the algorithm—most commonly, at the start of each loop iteration. Invariants are the bridge between “local steps” and “global correctness.”

Strong invariants typically describe:

• What portion of the work has already been completed.
• How variables relate to the original input.
• Bounds and safety properties (e.g., indices stay in range).

Invariants must be:

• True initially (before the first iteration).
• Preserved (if true at the start of an iteration, still true at the start of the next).
• Useful at termination (combined with the loop stopping condition, they imply the postcondition).

A Complete Worked Example: Summing the First n Integers

We will prove correct an algorithm that computes 1 + 2 + ... + n for a nonnegative integer n.

Algorithm (Pseudocode)

sum = 0
k = 1
while k <= n:
    sum = sum + k
    k = k + 1
return sum

Step 1: Write Preconditions and Postconditions

Precondition: n is an integer and n >= 0.

Postcondition: the returned value sum equals 1 + 2 + ... + n. (If n = 0, this sum is 0.)

Step 2: Propose a Loop Invariant

We need an invariant that captures what sum represents as the loop progresses. A good candidate:

Invariant (I): At the start of each loop iteration, sum = 1 + 2 + ... + (k - 1).

This says: before processing k, we have already accumulated everything up to k-1.

Step 3: Prove the Invariant Holds Initially

Before the first iteration, the algorithm sets sum = 0 and k = 1.

Check invariant: 1 + 2 + ... + (k - 1) becomes 1 + 2 + ... + 0, which is defined as 0. That matches sum = 0. So the invariant is true initially.

Step 4: Prove the Invariant Is Preserved (Maintenance)

Assume the invariant is true at the start of some iteration with current values sum and k. That means:

sum = 1 + 2 + ... + (k - 1).

The loop body executes:

• sum = sum + k
• k = k + 1

Let the old values be sum_old and k_old. After the first assignment:

sum_new = sum_old + k_old = (1 + 2 + ... + (k_old - 1)) + k_old = 1 + 2 + ... + k_old.

After incrementing k:

k_new = k_old + 1, so k_new - 1 = k_old.

Rewrite the invariant target for the next iteration:

We need sum_new = 1 + 2 + ... + (k_new - 1). But (k_new - 1) = k_old, and we already derived sum_new = 1 + 2 + ... + k_old. Therefore the invariant holds at the start of the next iteration.

Step 5: Use Termination to Derive the Postcondition

The loop stops when k > n. At that moment, the invariant is still true (it holds at the start of each iteration; when the loop condition fails, we are at the point just after the last iteration, with the invariant still describing the relationship that has been maintained).

From the loop exit condition k > n and the fact that k increases by 1 starting from 1, the first time it becomes greater than n is when k = n + 1.

Plug into the invariant:

sum = 1 + 2 + ... + (k - 1) = 1 + 2 + ... + n.

This is exactly the postcondition, so the algorithm is correct under the precondition.

What This Proof Did (Checklist)

How to Invent Useful Invariants

Many learners get stuck not on the proof steps, but on writing the invariant. Here are practical patterns:

1) “Processed prefix” pattern

Common when scanning arrays or lists.

• Example invariant: “All elements in positions 0..i-1 have been examined, and best equals the maximum among them.”

2) “Partial construction” pattern

Common when building an output gradually.

• Example invariant: “The output list contains exactly the transformed versions of the first i input items.”

3) “Conservation” pattern

Useful when rearranging items.

• Example invariant: “The multiset of elements in arr is unchanged from the start.”

4) “Bounds and safety” pattern

Often needed in addition to the main progress claim.

• Example invariant: “0 <= i <= len(arr)” to ensure indexing stays valid.

Common Logical Pitfalls (and How to Avoid Them)

Missing cases in the specification

Pitfall: writing a postcondition that ignores edge cases like empty inputs, n = 0, duplicates, or negative values.

Fix: explicitly decide what should happen in edge cases and encode it in pre/postconditions. If you don’t want to handle a case, make it a precondition (e.g., len(arr) > 0).

Assuming what you need to prove

Pitfall: using the postcondition inside the proof of the invariant (“since the algorithm returns the right sum, ...”).

Fix: only use the precondition, the algorithm’s assignments, and previously established facts (like the invariant hypothesis during maintenance).

Invariant that is true but useless

Pitfall: choosing an invariant like “k is an integer” or “sum >= 0” that doesn’t help derive the postcondition.

Fix: ensure the invariant connects the evolving variables to the desired result (e.g., sum equals a partial sum).

Off-by-one errors in invariants

Pitfall: writing sum = 1 + ... + k when the loop is about to add k, causing the maintenance step to fail.

Fix: decide whether the invariant is stated at the start or end of each iteration, and match the formula to that moment. Use “up to k-1” style when k is the next item to process.

Confusing termination with correctness

Pitfall: proving the loop stops, then assuming the result is correct.

Fix: termination only means it finishes; correctness requires the invariant-to-postcondition implication at the stopping point. (In many problems you need both: a termination argument and a correctness argument.)

Forgetting to justify that the exit condition gives the right final index/value

Pitfall: at loop exit, using “k = n+1” without justification.

Fix: argue why the loop must stop exactly there (monotonic change + condition). If the loop can skip values or change by more than 1, you need a different argument.

Practice Problems (Write Preconditions, Postconditions, and Invariants)

For each problem: (1) write a precondition, (2) write a postcondition, (3) propose one or more loop invariants stated at the start of each iteration, and (4) briefly explain how the invariant plus loop exit implies the postcondition.

1) Count occurrences

count = 0
i = 0
while i < len(arr):
    if arr[i] == target:
        count = count + 1
    i = i + 1
return count

• Hint invariant: relate count to how many matches appear in arr[0..i-1].

2) Find maximum (non-empty array)

best = arr[0]
i = 1
while i < len(arr):
    if arr[i] > best:
        best = arr[i]
    i = i + 1
return best

• Hint invariant: best is the maximum of the prefix already scanned.
• Also consider a safety invariant about i staying within bounds.

3) Compute integer power (nonnegative exponent)

result = 1
k = 0
while k < exp:
    result = result * base
    k = k + 1
return result

• Hint invariant: result = base^k at the start of each iteration.

4) Prefix sum array

prefix = new array of length len(arr)
running = 0
i = 0
while i < len(arr):
    running = running + arr[i]
    prefix[i] = running
    i = i + 1
return prefix

• Hint invariant: for all indices j in 0..i-1, prefix[j] equals the sum of arr[0..j], and running equals the sum of arr[0..i-1].

5) Linear search with “not found” result

i = 0
while i < len(arr) and arr[i] != target:
    i = i + 1
if i == len(arr):
    return -1
else:
    return i

• Hint invariant: all elements in arr[0..i-1] are not equal to target.
• Be explicit in the postcondition about what -1 means.