Invariant Inference

Overview

Analyze loops and automatically infer invariants—properties that remain true throughout loop execution. Generate these as code assertions for verification and correctness proofs.

Workflow

1. Identify the Loop

First, locate and understand the loop to analyze:

Loop types to recognize:

for loops with index variables
while loops with conditions
do-while loops
Iterator-based loops
Recursive functions (treated as implicit loops)

Extract key information:

Loop variable(s) and their initial values
Loop condition (when it terminates)
Loop body (what happens each iteration)
Variables modified in the loop
Variables read but not modified

2. Analyze Loop Structure

Understand what the loop does:

Categorize the loop:

Accumulation: Building up a sum, product, or collection
Search: Looking for an element or condition
Transformation: Modifying elements in a data structure
Generation: Creating new data based on input
Traversal: Visiting all elements
Sorting/Partitioning: Rearranging elements

Identify patterns:

Array/list iteration with bounds
Counter increments/decrements
Pointer advancement
Collection building
Flag-based early termination

3. Infer Invariant Categories

Generate invariants for each applicable category. See invariant-patterns.md for comprehensive patterns.

Bounds Invariants

Properties about variable ranges:

# Loop: for i in range(n)
assert 0 <= i < n

# Loop: while i < len(arr)
assert 0 <= i <= len(arr)

# Loop: two pointers
while left < right:
    assert 0 <= left <= right < len(arr)

Relationship Invariants

Properties relating variables:

Sum/Accumulation:

total = 0
for i in range(len(arr)):
    assert total == sum(arr[0:i])  # Invariant before update
    total += arr[i]
assert total == sum(arr)  # Post-condition

Max/Min:

max_val = arr[0]
for i in range(1, len(arr)):
    assert max_val == max(arr[0:i])
    if arr[i] > max_val:
        max_val = arr[i]

Product:

product = 1
for i in range(len(arr)):
    assert product == arr[0] * arr[1] * ... * arr[i-1]
    product *= arr[i]

Progress Invariants

Properties showing termination:

# Decreasing to zero
while n > 0:
    assert n > 0  # Still positive
    n -= 1
    assert n >= 0  # Non-negative after decrement

# Increasing to limit
i = 0
while i < n:
    assert i < n  # Not yet at limit
    i += 1
    assert i <= n  # At most n

Data Structure Invariants

Properties about structure integrity:

Sorted sublists:

# Insertion sort
for i in range(1, len(arr)):
    assert is_sorted(arr[0:i])  # Prefix is sorted
    # ... insert arr[i] into sorted position

Partition property:

# Partitioning around pivot
while left < right:
    assert all(arr[j] <= pivot for j in range(0, left))
    assert all(arr[j] >= pivot for j in range(right, len(arr)))
    # ... move pointers

Size invariants:

result = []
for i in range(len(items)):
    assert len(result) == i  # Processed i items so far
    if condition(items[i]):
        result.append(items[i])

4. Generate Assertions

Convert inferred invariants into code assertions:

Python Format

def find_maximum(arr):
    """Find maximum element in array."""
    assert len(arr) > 0, "Array must not be empty"  # Pre-condition

    max_val = arr[0]

    for i in range(1, len(arr)):
        # Loop invariants
        assert 0 < i < len(arr), "Index in valid range"
        assert max_val == max(arr[0:i]), "max_val is maximum so far"
        assert max_val in arr[0:i], "max_val is from processed elements"

        if arr[i] > max_val:
            max_val = arr[i]

    assert max_val == max(arr), "max_val is maximum of entire array"  # Post-condition
    return max_val

Java Format

public int findMaximum(int[] arr) {
    assert arr.length > 0 : "Array must not be empty";

    int maxVal = arr[0];

    for (int i = 1; i < arr.length; i++) {
        assert i > 0 && i < arr.length : "Index in valid range";
        assert maxVal == max(arr, 0, i) : "maxVal is maximum so far";

        if (arr[i] > maxVal) {
            maxVal = arr[i];
        }
    }

    assert maxVal == max(arr, 0, arr.length) : "maxVal is maximum";
    return maxVal;
}

C/C++ Format

int find_maximum(int arr[], int n) {
    assert(n > 0);  // Pre-condition

    int max_val = arr[0];

    for (int i = 1; i < n; i++) {
        assert(i >= 1 && i < n);  // Bounds
        assert(max_val >= arr[0]);  // max_val is at least first element
        // Note: Can't easily express "max of subarray" in C without helper

        if (arr[i] > max_val) {
            max_val = arr[i];
        }
    }

    return max_val;
}

5. Verify Invariants

Check that inferred invariants are correct:

Initialization

Invariant must be true before the loop starts:

# Loop: total = 0; for i in range(n): total += arr[i]
# Invariant: total == sum(arr[0:i])
# Check: Before loop, i=0, total=0, sum(arr[0:0])=0 ✓

Maintenance

Invariant remains true after each iteration:

# Assume invariant true at start of iteration i
# Show it's true at start of iteration i+1
# Before: total == sum(arr[0:i])
# Execute: total += arr[i]
# After: total == sum(arr[0:i]) + arr[i] == sum(arr[0:i+1]) ✓

Termination

Invariant + termination condition proves post-condition:

# After loop: i == n (termination) and total == sum(arr[0:i]) (invariant)
# Therefore: total == sum(arr[0:n]) == sum(arr) ✓

6. Handle Complex Cases

Nested Loops

Generate invariants for each nesting level:

# Matrix sum
total = 0
for i in range(rows):
    assert total == sum(matrix[0:i, :])  # Outer invariant

    for j in range(cols):
        assert total == sum(matrix[0:i, :]) + sum(matrix[i, 0:j])  # Inner
        total += matrix[i][j]

Multiple Variables

Track relationships between variables:

# Two pointers
left, right = 0, len(arr) - 1
while left < right:
    assert 0 <= left <= right < len(arr)
    assert left + right == len(arr) - 1  # Relationship invariant
    # (only true if they move symmetrically)
    left += 1
    right -= 1

Early Exit

Handle break/return statements:

# Search with early exit
found = False
for i in range(len(arr)):
    assert not found or arr[i-1] == target  # If found, previous element was it

    if arr[i] == target:
        found = True
        break

assert not found or target in arr[0:i+1]  # Post-condition

Loop with Side Effects

Track effects on external state:

# Modifying a list
for i in range(len(arr)):
    assert len(arr) remains constant  # Size doesn't change
    assert arr[0:i] are processed correctly
    arr[i] = transform(arr[i])

Example Workflows

Example 1: Simple Accumulation

User request:

"Infer invariants for this sum loop"

def array_sum(arr):
    total = 0
    for i in range(len(arr)):
        total += arr[i]
    return total

Response:

def array_sum(arr):
    assert len(arr) >= 0  # Pre-condition: valid array

    total = 0
    for i in range(len(arr)):
        # Loop invariants
        assert 0 <= i < len(arr), "Index in valid range"
        assert total == sum(arr[0:i]), "total is sum of elements so far"

        total += arr[i]

    assert total == sum(arr), "total is sum of entire array"  # Post-condition
    return total

Explanation:

Bounds: 0 <= i < len(arr)
Relationship: total == sum(arr[0:i])
Progress: i increases each iteration
Post-condition follows from invariant + termination

Example 2: Search Loop