3.3 Program Correctness: Specifications, Loop Invariants, and Termination

"The function passes all tests" is not the same as "the function satisfies its specification." Testing, static analysis, model checking, and formal proof provide different scopes of evidence. Program correctness begins with a clear statement of which property we intend to prove.

Start with Preconditions and Postconditions

Hoare triple notation:

{P} C {Q}

• P: the precondition that must hold before executing command C;
• C: the program or statement;
• Q: the postcondition that must hold if the execution completes as specified.

For example:

{amount > 0 ∧ balance ≥ amount}
balance := balance - amount
{balance ≥ 0}

The triple does not automatically guarantee that the caller provides valid amount, nor does it ensure that the program terminates. Responsibility for specifications is divided: the caller is responsible for establishing the precondition, while the called program is responsible for ensuring the postcondition.

The initial model concerns sequential execution and normal completion. Specify separately how exceptions, concurrent interference, and undefined behavior are treated; a normal-return postcondition must not hide an exceptional outcome that the specification should forbid.

Partial and Total Correctness

Partial correctness: If a program terminates, its result satisfies the postcondition.

Total correctness: The program terminates, and its result satisfies the postcondition.

int zero() {
    while (true) { }
}

The statement "if the function returns, it returns 0" might logically hold as a partial correctness assertion since the function never returns, but it clearly fails total correctness, as the function does not ultimately return 0.

Production specifications may also include requirements for time, memory, concurrency, and fault tolerance. Mathematical functional correctness does not guarantee system availability under resource constraints.

Assignment Changes State

To ensure that after executing:

x := x + 1

the condition x>0 holds, what must be true before the execution? Substitute the postcondition's new value of x with the assignment expression:

x + 1 > 0
⇔ x > -1

This is a backward reasoning approach to derive the precondition. Multiple statements can be traversed backward from the final goal, but branches, loops, and exceptions introduce additional proof obligations.

This calculation uses mathematical integers without overflow. For Java int, x=Integer.MAX_VALUE satisfies x>-1 but overflows on increment and violates the postcondition. The machine statement requires 0≤x<Integer.MAX_VALUE to guarantee a positive result.

Branches Must Cover Both Paths

int abs(int x) {
    if (x >= 0) return x;
    return -x;
}

To prove that the return value is non-negative, we must consider both:

• x≥0 path returns x;
• x<0 path returns -x.

We must also account for integer overflow: in Java, -Integer.MIN_VALUE remains negative. If the specification claims that every int input produces a non-negative return value, the actual source code fails this requirement. Solutions include tightening the precondition, using a wider integer type, or explicitly handling overflow.

The difference between mathematical integers and machine integers must be incorporated into the model.

If the return type can be long, use return -(long) x; in the negative branch. Widening before negation maps the minimum int to 2147483648L. With (long) (-x), negation has already overflowed in int.

Loop Invariant Holds Across Each Iteration

Consider computing the prefix sum of an array:

Assume values != null and no concurrent mutation of its contents. The postcondition returns the mathematical sum of all int elements in the entry snapshot. This is a method to place inside a Java class:

long sum(int[] values) {
    long total = 0;
    int i = 0;
    while (i < values.length) {
        total += values[i];
        i++;
    }
    return total;
}

Let n=values.length. A loop invariant is:

0 ≤ i ≤ values.length
total = values[0] + ... + values[i-1]

The proof proceeds in three steps:

1. Initialization: Before the loop begins, i=0,total=0, and the prefix sum of an empty array is 0;
2. Maintenance: If the invariant holds before an iteration and i<n, then adding values[i] to the total and incrementing i by one preserves the invariant;
3. Termination: The exit condition gives i≥n, which combined with the invariant's i≤n yields i=n, so total is the sum of the entire array.

The invariant is not a goal that becomes true only at the end of the loop; it is a bridge that holds true at every check of the loop condition.

The long accumulator also needs an overflow argument. A Java array has at most 2³¹−1 elements, each int has magnitude at most 2³¹, and every prefix sum therefore has magnitude below 2⁶², within long range. This depends on both the element type and array-length bound; it does not carry over to long[]. See JLS 21 on integral types and array members.

Termination Requires a Decreasing Quantity

To prove a loop terminates, look for a variant (ranking function) that satisfies:

• Takes values in a well-founded set, commonly non-negative integers;
• Strictly decreases on each iteration;
• Cannot decrease infinitely.

In the example above, we use:

values.length - i

Each iteration increases i by 1, so the variant decreases by 1. The guard i<n ensures the variant is positive when the loop begins.

Not all termination proofs can be captured by a single integer. Recursive functions, graph traversals, and concurrent protocols may require more sophisticated measures, such as lexicographic ordering, multiset orderings, or fairness assumptions.

A decreasing measure also depends on termination of the loop body and assumptions about execution. An outer counter cannot prove return if the body waits indefinitely for a network response. Dafny’s termination tutorial explains concrete decreases rules.

The Invariant in Binary Search

When searching for a target in a sorted array, we can maintain a half-open interval [low, high):

0 ≤ low ≤ high ≤ n
If the target exists, it must lie within [low, high)

After each choice of mid:

• If a[mid] < target, set low=mid+1;
• If a[mid] > target, set high=mid;
• Otherwise, return mid.

Every continuing branch strictly decreases high-low, while a match returns immediately, ensuring termination. Upon exit, low=high, the candidate interval is empty, and we can conclude that the target does not exist.

Using a half-open interval is not the only correct approach, but the index definitions, guards, and updates must all belong to the same invariant. Mixing closed and half-open intervals is a common source of array out-of-bounds errors or infinite loops in binary search implementations.

This complete Python 3 example requires a nondecreasing integer list that is not mutated concurrently. With duplicates, any matching index is allowed:

def binary_search(values, target):
    low, high = 0, len(values)
    while low < high:
        mid = low + (high - low) // 2
        if values[mid] < target:
            low = mid + 1
        elif values[mid] > target:
            high = mid
        else:
            return mid
    return -1

print(binary_search([], 3))              # -1
print(binary_search([1, 2], 1))           # 0
print(binary_search([1, 2, 2, 4], 2))     # 2: any matching index is allowed.
print(binary_search([1, 2], 3))           # -1

mid=low+(high-low)//2 lies inside the nonempty candidate interval and also avoids summing both bounds in fixed-width implementations. Changing the greater-than branch to high=mid-1 would miss index 0 when searching for 1 in [1,2]. This function does not scan to validate ordering; the caller must establish that precondition.

Testing and Proof Provide Different Evidence

"The test can only find bugs, not prove the absence of bugs" is an overgeneralization. If the input domain is finite and testing exhaustively covers all states, testing can prove properties within that model scope. Model checking can also exhaustively explore finite state spaces. The issue lies in the fact that real-world systems typically have vast input domains, complex timing, and concurrent states, making test coverage only part of the state space.

Method	Strengths	Limitations
Unit/Example Testing	Specific behavior, regression detection	Limited coverage
Property-Based Testing	Generates large volumes of inputs, narrows down counterexamples	Still not exhaustive across all cases
Fuzz Testing	Uncovers unexpected inputs and parser defects	Difficult to express complete functional specifications
Static Analysis	No runtime execution; covers multiple execution paths	Abstractions may lead to false positives or negatives
Model Checking	Exhaustively explores finite model states	State explosion, model inaccuracies
Deductive Proof	Provides general guarantees based on specifications	Specifications, tools, or trusted foundations may themselves be flawed

Reliable engineering typically combines multiple forms of evidence. Proving core algorithms does not replace integration testing. Testing external dependencies does not substitute for invariant reasoning.

A Wrong Specification Can Still Be Proved

Proof tools can only verify whether an implementation satisfies a given specification. If the specification omits a constraint like "no other account may be modified," a transfer function that clears all accounts and sets the target balance might still satisfy a weak, locally valid postcondition.

Specification reviews should examine:

• Normal outcomes;
• Errors and exceptions;
• Unchanged state;
• Boundaries and overflow conditions;
• Termination and resource limits;
• Assumptions about concurrent environments.

The greatest benefit from formalization often comes during the specification phase: vague requirements are forced into concrete, discussable conditions.

Completion Checklist

Specify and analyze a function that returns the maximum value of an array:

1. Specify how to handle empty arrays and the preconditions for this operation;
2. Define the postconditions: the result must be an element of the array and must be greater than or equal to every other element;
3. State the invariant of the scanning loop;
4. Provide a termination variant;
5. Indicate whether integer types, concurrent modifications, or exceptions are modeled;
6. Design example tests, property-based tests, and one static or formal verification check.

References

• Software Foundations: Program Verification
• Dafny Documentation