source: CIVL/examples/loop_invariants/selectSort-bad_think.cvl@ fecbb5a

#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);
  /* Following loop invariants is incorrect, one either needs to
     specify minIdx in loop invariants or put the minIdx inside the
     loop. The previous prototype relies upon the correct
     specification of loop assigns, it cannot detect this. */   

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