source: CIVL/examples/loop_invariants/dev/selectSort.cvl

#include <assert.h>
#pragma CIVL ACSL
$input int N;
$assume(N > 0);
int a[N];

int main() {
  int i, j;
  int minIdx = 0;
  
  $havoc(&a);
  
  /*@ loop invariant 0 <= i && i <= N;
    @ loop invariant \forall int t; N-i+1<=t && t <N  ==>
    @                  a[t] <= a[t-1];
    @ loop invariant \forall int t; 0 <= t && t < N-i && i > 0 ==>
    @                  a[t] >= a[N-i];
    @ loop assigns i, j, a[0 .. N-1];
    @*/
  for (i = 0; i < N; i++) {
    /*@ loop invariant 0<=j && j <=N-i && 0<=minIdx && 
      @                minIdx<N-i;
      @ loop invariant \forall int t; 0<=t && t <j ==>
      @                               a[t] >= a[minIdx];
      @ loop assigns j, minIdx;
      @*/
    for (j = 0; j < N-i; j++)
      if (a[j] < a[minIdx])
        minIdx = j;
    
    int tmp = a[minIdx];
      
    a[minIdx] = a[N-i-1];
    a[N-i-1] = tmp;
    minIdx = 0;
  }
  assert($forall (int i : 1 .. N-1) a[i] <= a[i-1]);
  return 0;
}