#include <limits.h>
#include "abs.h"

/*@ 
 requires 1 < n <= UINT_MAX;
 requires \valid_read(tab+(0..n-1));
 requires \forall integer i; 0 <= i < n ==> (INT_MIN / 2 <= tab[i] <=  INT_MAX/2);
 terminates \true;
 assigns \nothing;
 ensures \forall integer i; 0 <= i < n ==> (\forall integer j; i < j < n ==> \result <= abs(tab[i]-tab[j]));
 */
int min_dist(int *tab, unsigned int n);