33 lines
853 B
C
33 lines
853 B
C
#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;
|
|
}
|