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
```python
while condition:
    # Need: invariant that holds before/after each iteration
    body
```

**Function Contracts**: For each function
```python
def function(params):
    # Need: precondition (what must be true on entry)
    body
    # Need: postcondition (what is guaranteed on exit)
```

**Assertions**: For verification points
```python
# 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
```python
i = 0
while i < n:
    # Inferred: 0 ≤ i < n
    i += 1
# Inferred: i = n
```

**Relational Analysis**: Infer relationships between variables
```python
i = 0
j = 0
while i < n:
    # Inferred: i = j
    i += 1
    j += 1
```

**Shape Analysis**: Infer data structure properties
```python
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**:
```python
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**:
```python
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**:
```python
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**:
```python
def get_element(arr, index):
    return arr[index]
```

**Generated Precondition**:
```
requires 0 ≤ index < len(arr)
requires arr is not None
```

**Division Function**:
```python
def divide(x, y):
    return x / y
```

**Generated Precondition**:
```
requires y ≠ 0
```

**Linked List Function**:
```python
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**:
```python
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**:
```python
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**:
```python
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**:
```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**:
```isabelle
lemma find_max_correct:
  assumes "length arr > 0"
  shows "find_max arr ∈ set arr ∧
         (∀x ∈ set arr. x ≤ find_max arr)"
```

**Coq**:
```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)**:
```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):
```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):
```dafny
method InsertionSort(arr: array<int>)
  requires arr.Length >= 0
  ensures sorted(arr[..])
  ensures multiset(arr[..])