abstract-invariant-generator

Abstract Invariant Generator

Overview

This skill uses abstract interpretation to automatically infer loop invariants, function preconditions, and postconditions. It generates formal specifications that support verification and reasoning about program correctness.

Invariant Generation Workflow

Step 1: Identify Specification Points

Analyze the code to identify where invariants are needed:

Loop Invariants: For each loop

while condition:
    # Need: invariant that holds before/after each iteration
    body

Function Contracts: For each function

def function(params):
    # Need: precondition (what must be true on entry)
    body
    # Need: postcondition (what is guaranteed on exit)

Assertions: For verification points

# Need: invariant that holds at this point
assert property

Step 2: Perform Abstract Interpretation

Use abstract domains to infer properties:

Interval Analysis: Infer numeric ranges

i = 0
while i < n:
    # Inferred: 0 ≤ i < n
    i += 1
# Inferred: i = n

Relational Analysis: Infer relationships between variables

i = 0
j = 0
while i < n:
    # Inferred: i = j
    i += 1
    j += 1

Shape Analysis: Infer data structure properties

while node is not None:
    # Inferred: node is in the linked list
    node = node.next

Step 3: Generate Loop Invariants

For each loop, generate an invariant that:

1. Holds before the loop (initialization)
2. Is preserved by the loop body (maintenance)
3. Combined with loop exit, implies desired property (termination)

Template-Based Generation:

Counter Loop:

i = 0
while i < n:
    arr[i] = 0
    i += 1

Generated Invariant:

invariant 0 ≤ i ≤ n
invariant ∀k. 0 ≤ k < i ⟹ arr[k] = 0

Accumulator Loop:

sum = 0
i = 0
while i < len(arr):
    sum += arr[i]
    i += 1

Generated Invariant:

invariant 0 ≤ i ≤ len(arr)
invariant sum = Σ(arr[0..i-1])