arabelatso/skills-4-se/abstract-invariant-generator

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

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

# Need: invariant that holds at this point
assert property

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

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

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

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

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

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

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

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

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

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

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

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

requires y ≠ 0

def get_next(node):
    return node.next

requires node is not None

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

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

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

ensures len(result) = len(arr)
ensures ∀i. 0 ≤ i < len(result)-1 ⟹ result[i] ≤ result[i+1]
ensures multiset(result) = multiset(arr)

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

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

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;
  }
}

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

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

/*@ 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;
}

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

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

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

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

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

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

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

invariant 0 ≤ i ≤ n

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

for i in range(n):
    for j in range(m):
        matrix[i][j] = 0

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

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

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