invariant-inference

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]