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

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

/*@ predicate permut(int * p, int * q, int l, int u);
  @*/

int main() {
  int i, j;

  $havoc(&a);
  memcpy(pre_a, a, N * sizeof(int));
  /*@ 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 invariant permut(a, pre_a, 0, N);
    @ loop assigns  i, j, a[0 .. N-1];  
    @*/
  for (i = 0; i < N; i++) {
    int minIdx = 0;
    /*@ 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   minIdx,  j;  
      @*/
    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;
  }
  $assert(permut(a, pre_a, 0, N) && $forall (int i : 1 .. N-1) a[i] <= a[i-1]);
  return 0;
}