3.3 Program Correctness: Specifications, Loop Invariants, and Termination

A program passes current tests, but the proof engineer in the tower still asks: "For inputs not covered by the tests, how can we be sure the program still satisfies its specification?"

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

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 worked forward from the final goal, but branches, loops, and exceptions introduce additional proof obligations.

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 all int returns a non-negative 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.

Loop Invariant Holds Across Each Iteration

Consider computing the prefix sum of an array:

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

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.

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.

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.

The length of the interval high-low strictly decreases, 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.

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 a fraction of the full landscape.

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.

Specifications Are Wrong, So the Proof Will Faithfully Prove the Wrong Thing

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

Complete the function for "returning the maximum value from 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