examples/micro-c/sort.c

   1
   2 // tri par insertion
   3
   4 #include <stdio.h>
   5 #include <stdlib.h>
   6
   7 void sort(int a[], int n)
   8 //@ requires length(a) == n >= 1;
   9 //@ ensures  forall i,j. 0 <= i <= j < n -> a[i] <= a[j];
  10 {
  11   for (int m = 1; m < n; m++) {
  12     //@ invariant 1 <= m <= n;
  13     //@ invariant forall i,j. 0 <= i <= j < m -> a[i] <= a[j];
  14     //@ variant   n - m;
  15     int x = a[m];
  16     int k;
  17     for (k = m; k > 0 && a[k-1] > x; k--) {
  18         //@ invariant 0 <= k <= m;
  19         //@ invariant forall i,j. 0 <= i <= j < k               -> a[i] <= a[j];
  20         //@ invariant forall i,j. 0 <= i      < k <      j <= m -> a[i] <= a[j];
  21         //@ invariant forall i,j.               k < i <= j <= m -> a[i] <= a[j];
  22         //@ invariant forall   j.               k <      j <= m -> x    <  a[j];
  23         //@ variant   k;
  24       a[k] = a[k-1];
  25     }
  26     a[k] = x;
  27   }
  28 }
  29
  30 int main() {
  31   int n = 42;
  32   int a[n];
  33   for (int i = 0; i < n; i++) {
  34     //@ invariant 0 <= i <= n;    //@ variant n - i;
  35     a[i] = rand() % 100;
  36     printf("%d, ", a[i]);
  37   }
  38   printf("\n");
  39   sort(a, n);
  40   for (int i = 0; i < n; i++)
  41     //@ invariant 0 <= i <= n;    //@ variant n - i;
  42     printf("%d, ", a[i]);
  43   printf("\n");
  44   return 0;
  45 }
  46