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])

Search Loop:

i = 0
found = False
while i < len(arr) and not found:
    if arr[i] == target:
        found = True
    else:
        i += 1

Generated Invariant:

invariant 0 ≤ i ≤ len(arr)
invariant ∀k. 0 ≤ k < i ⟹ arr[k] ≠ target
invariant found ⟹ arr[i] = target

Step 4: Generate Function Preconditions

Infer what must be true for the function to work correctly:

Array Access Function:

def get_element(arr, index):
    return arr[index]

Generated Precondition:

requires 0 ≤ index < len(arr)
requires arr is not None

Division Function:

def divide(x, y):
    return x / y

Generated Precondition:

requires y ≠ 0

Linked List Function:

def get_next(node):
    return node.next

Generated Precondition:

requires node is not None

Step 5: Generate Function Postconditions

Infer what the function guarantees on exit:

Maximum Function:

def find_max(arr):
    max_val = arr[0]
    for i in range(1, len(arr)):
        if arr[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 < len(result)-1 ⟹ result[i] ≤ result[i+1]
ensures multiset(result) = multiset(arr)

Search Function:

def binary_search(arr, target):
    # ... search logic ...
    return index

Generated Postcondition:

ensures result = -1 ∨ (0 ≤ result < len(arr) ∧ arr[result] = target)
ensures result ≠ -1 ⟹ arr[result] = target
ensures result = -1 ⟹ target ∉ arr

Step 6: Express in Target Language

Format invariants for the target verification system:

Dafny:

method FindMax(arr: array<int>) returns (max: int)
  requires arr.Length > 0
  ensures max in arr[..]
  ensures forall i :: 0 <= i < arr.Length ==> arr[i] <= max
{
  max := arr[0];
  var i := 1;
  while i < arr.Length
    invariant 1 <= i <= arr.Length
    invariant max in arr[..i]
    invariant forall k :: 0 <= k < i ==> arr[k] <= max
  {
    if arr[i] > 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 <= find_max arr).

ACSL (for C):

/*@ requires n > 0;
  @ requires \valid(arr + (0..n-1));
  @ ensures \result >= 0 && \result < n;
  @ ensures \forall integer k; 0 <= k < n ==> arr[k] <= arr[\result];
  @*/
int find_max(int arr[], int n) {
  int max_idx = 0;
  /*@ loop invariant 1 <= i <= n;
    @ loop invariant 0 <= max_idx < i;
    @ loop invariant \forall integer k; 0 <= k < i ==> arr[k] <= arr[max_idx];
    @ loop variant n - i;
    @*/
  for (int i = 1; i < n; i++) {
    if (arr[i] > 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<int>)
  requires arr.Length >= 0
  ensures sorted(arr[..])
  ensures multiset(arr[..]) == multiset(old(arr[..]))
  modifies arr
{
  var i := 1;
  while i < arr.Length
    invariant 1 <= i <= arr.Length
    invariant sorted(arr[..i])
    invariant multiset(arr[..]) == multiset(old(arr[..]))
  {
    var key := arr[i];
    var j := i - 1;

    while j >= 0 && arr[j] > key
      invariant -1 <= j < i
      invariant sorted(arr[..j+1])
      invariant sorted(arr[j+2..i+1])
      invariant forall k :: j+2 <= k <= i ==> 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<int>) {
  forall i, j :: 0 <= i < j < |s| ==> s[i] <= s[j]
}

Explanation:

Outer Loop Invariants:

1. 1 <= i <= arr.Length: Loop counter bounds
2. sorted(arr[..i]): First i elements are sorted
3. multiset(arr[..]) == multiset(old(arr[..])): Permutation preservation

Inner Loop Invariants:

1. -1 <= j < i: Loop counter bounds
2. sorted(arr[..j+1]): Elements before j+1 remain sorted
3. sorted(arr[j+2..i+1]): Shifted elements remain sorted
4. forall k :: j+2 <= k <= 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:

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