31 lines
882 B
C
31 lines
882 B
C
#include <limits.h>
|
|
#include "abs.h"
|
|
/*@
|
|
requires 0 < n < INT_MAX;
|
|
requires \valid_read(tab+(0..n-1));
|
|
requires \forall integer a,b; 0 <= a < b < n ==> tab[a] - tab[b] <= INT_MAX;
|
|
ensures \forall integer a,b; 0 <= a < b < n ==> \result >= abs(tab[a]-tab[b]);
|
|
*/
|
|
int max_dist ( int *tab, int n)
|
|
{
|
|
int max = tab[0];
|
|
int min = tab[0];
|
|
unsigned int i = 1;
|
|
/*@
|
|
loop assigns i, max, min;
|
|
loop invariant I1: \at(i, LoopEntry) <= i <= n;
|
|
loop invariant I2: min <= max;
|
|
loop invariant I3: \forall integer j; (\at(i, LoopEntry) <= j < i ==> max >= tab[j] >= min);
|
|
loop variant n - i;
|
|
*/
|
|
|
|
while ( i < n)
|
|
{
|
|
if ( tab[i] > max) max = tab[i];
|
|
if ( tab[i] < min) min = tab[i];
|
|
i++;
|
|
}
|
|
//@ assert INT_MIN <= max <= INT_MAX;
|
|
//@ assert INT_MIN <= min <= INT_MAX;
|
|
return max - min;
|
|
}
|