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  max_val:
            max_val = arr[i]
    return max_val

Generated Postcondition:

ensures result ∈ arr
ensures ∀x ∈ arr. x ≤ result

Sorting Function:

def sort(arr):
    # ... sorting logic ...
    return sorted_arr

Generated Postcondition:

ensures len(result) = len(arr)
ensures ∀i. 0 ≤ i ) returns (max: int)
  requires arr.Length > 0
  ensures max in arr[..]
  ensures forall i :: 0  arr[i]  arr[k]  max {
      max := arr[i];
    }
    i := i + 1;
  }
}

Isabelle/HOL:

lemma find_max_correct:
  assumes "length arr > 0"
  shows "find_max arr ∈ set arr ∧
         (∀x ∈ set arr. x ≤ find_max arr)"

Coq:

Lemma find_max_correct : forall (arr : list nat),
  length arr > 0 ->
  In (find_max arr) arr /\
  (forall x, In x arr -> x  0;
  @ requires \valid(arr + (0..n-1));
  @ ensures \result >= 0 && \result  arr[k]  arr[k]  arr[max_idx]) {
      max_idx = i;
    }
  }
  return max_idx;
}

Complete Example

Input Code (Python):

def insertion_sort(arr):
    for i in range(1, len(arr)):
        key = arr[i]
        j = i - 1
        while j >= 0 and arr[j] > key:
            arr[j + 1] = arr[j]
            j -= 1
        arr[j + 1] = key

Analysis:

Outer Loop (for i in range(1, len(arr))):

• i ranges from 1 to len(arr)
• After each iteration, arr[0..i] is sorted
• Elements are permutation of original

Inner Loop (while j >= 0 and arr[j] > key):

• j decreases from i-1 to -1
• Shifts elements greater than key to the right
• Maintains: arr[j+2..i+1] contains elements > key

Generated Invariants (Dafny):

method InsertionSort(arr: array)
  requires arr.Length >= 0
  ensures sorted(arr[..])
  ensures multiset(arr[..]) == multiset(old(arr[..]))
  modifies arr
{
  var i := 1;
  while i = 0 && arr[j] > key
      invariant -1  arr[k] > key
      invariant multiset(arr[..]) == multiset(old(arr[..]))
    {
      arr[j + 1] := arr[j];
      j := j - 1;
    }

    arr[j + 1] := key;
    i := i + 1;
  }
}

predicate sorted(s: seq) {
  forall i, j :: 0  s[i]  arr[k] > key`: Shifted elements are greater than key
5. `multiset(arr[..]) == multiset(old(arr[..]))`: Permutation preservation

## Invariant Patterns

### Numeric Bounds

invariant 0 ≤ i ≤ n invariant low ≤ mid ≤ high

### Array Properties

invariant ∀k. 0 ≤ k < i ⟹ P(arr[k]) invariant sorted(arr[0..i]) invariant arr[i] = max(arr[0..i])

### Relationships

invariant i + j = n invariant i = 2 * j invariant sum = Σ(arr[0..i-1])

### Data Structure Properties

invariant acyclic(list) invariant node ∈ reachable(head) invariant size(tree) = n

### Permutation

invariant multiset(arr) = multiset(old(arr)) invariant set(arr) = set(old(arr))

## Strengthening Weak Invariants

Sometimes initial invariants are too weak. Strengthen them:

**Weak**:

invariant 0 ≤ i ≤ n

**Strengthened**:

invariant 0 ≤ i ≤ n invariant ∀k. 0 ≤ k < i ⟹ processed(arr[k])

**Technique**: Add properties about what has been accomplished so far.

## Handling Complex Loops

### Nested Loops

Generate invariants for each level:
```python
for i in range(n):
    for j in range(m):
        matrix[i][j] = 0

Invariants:

Outer loop:
  invariant 0 ≤ i ≤ n
  invariant ∀r. 0 ≤ r < i ⟹ (∀c. 0 ≤ c < m ⟹ matrix[r][c] = 0)

Inner loop:
  invariant 0 ≤ j ≤ m
  invariant ∀c. 0 ≤ c < j ⟹ matrix[i][c] = 0

Multiple Exit Conditions

Handle all exit paths:

while i < n and not found:
    if arr[i] == target:
        found = True
    i += 1

Invariants:

invariant 0 ≤ i ≤ n
invariant found ⟹ arr[i-1] = target
invariant ¬found ⟹ (∀k. 0 ≤ k < i ⟹ arr[k] ≠ target)

References

For detailed invariant generation techniques and patterns:

• references/loop_invariants.md: Loop invariant patterns and generation strategies
• references/function_contracts.md: Precondition and postcondition inference
• references/invariant_templates.md: Common invariant templates by algorithm type
• references/verification_languages.md: Syntax for different verification systems

Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

• Author: ArabelaTso
• Source: ArabelaTso/Skills-4-SE
• License: Apache-2.0
• Homepage: https://ArabelaTso.github.io/Skills-4-SE/

Install and usage instructions live in the source repository linked above.