#include "min_dist.h"
int min_dist(int *tab, unsigned int n)
{
    int min = abs(tab[0] - tab[1]);
    unsigned int i = 0;
    /*@
        loop invariant I1: \at(i, LoopEntry) <= i < n - 1;
        loop invariant I2: \exists integer k; (k == n - 1 ==> \at(min, LoopCurrent) >= min);
        loop assigns i, min;
        loop variant n - i;
    */
    while (i < n - 1)
    {
        int min_i = abs(tab[i] - tab[i + 1]);
        unsigned int j = i + 2;
        /*@
            loop invariant J1: \at(j, LoopEntry) <= j < n;
            loop assigns i, j , min, min_i;
            loop variant n - j;
        */
        while (j < n)
        {
            int d = abs(tab[i] - tab[j]);
            if (d < min_i)
                min_i = d;
            j++;
        }
        if (min_i < min)
            min = min_i;
        i++;
    }
    return min;
}