|
/* Generated by Frama-C */
|
|
typedef int value_type;
|
|
typedef unsigned int size_type;
|
|
/*@ requires \valid(p);
|
|
requires \valid(q);
|
|
ensures *\old(p) == \old(*q);
|
|
ensures *\old(q) == \old(*p);
|
|
assigns *p, *q;
|
|
*/
|
|
void swap(value_type *p, value_type *q);
|
|
|
|
/*@
|
|
predicate EqualRanges{K, L}(value_type *a, integer n, value_type *b) =
|
|
\forall integer i; 0 <= i < n ==> \at(*(a + i),K) == \at(*(b + i),L);
|
|
*/
|
|
/*@
|
|
predicate EqualRanges{K, L}
|
|
(value_type *a, integer m, integer n, value_type *b) =
|
|
\forall integer i; m <= i < n ==> \at(*(a + i),K) == \at(*(b + i),L);
|
|
*/
|
|
/*@
|
|
predicate EqualRanges{K, L}
|
|
(value_type *a, integer m, integer n, value_type *b, integer p) =
|
|
EqualRanges{K, L}(a + m, n - m, b + p);
|
|
*/
|
|
/*@
|
|
predicate EqualRanges{K, L}(value_type *a, integer m, integer n, integer p) =
|
|
EqualRanges{K, L}(a, m, n, a, p);
|
|
*/
|
|
/*@
|
|
predicate Unchanged{K, L}(value_type *a, integer m, integer n) =
|
|
\forall integer i; m <= i < n ==> \at(*(a + i),K) == \at(*(a + i),L);
|
|
*/
|
|
/*@
|
|
predicate Unchanged{K, L}(value_type *a, integer n) = Unchanged{K, L}(a, 0, n);
|
|
*/
|
|
/*@
|
|
axiomatic Count {
|
|
logic integer Count{L}(value_type *a, integer m, integer n, value_type v) =
|
|
n <= m? 0: Count(a, m, n - 1, v) + (*(a + (n - 1)) == v? 1: 0);
|
|
|
|
lemma CountSectionEmpty{L}:
|
|
\forall value_type *a, int v, integer m, integer n;
|
|
n <= m ==> Count(a, m, n, v) == 0;
|
|
|
|
lemma CountSectionHit{L}:
|
|
\forall value_type *a, int v, integer n, integer m;
|
|
m < n ==>
|
|
*(a + (n - 1)) == v ==> Count(a, m, n, v) == Count(a, m, n - 1, v) + 1;
|
|
|
|
lemma CountSectionMiss{L}:
|
|
\forall value_type *a, int v, integer n, integer m;
|
|
m < n ==>
|
|
*(a + (n - 1)) != v ==> Count(a, m, n, v) == Count(a, m, n - 1, v);
|
|
|
|
lemma CountSectionRead{K, L}:
|
|
\forall value_type *a, int v, integer m, integer n;
|
|
Unchanged{K, L}(a, m, n) ==> Count{K}(a, m, n, v) == Count{L}(a, m, n, v);
|
|
|
|
}
|
|
*/
|
|
/*@
|
|
logic integer Count{L}(value_type *a, integer n, value_type v) =
|
|
Count(a, 0, n, v);
|
|
*/
|
|
/*@
|
|
lemma CountEmpty{L}:
|
|
\forall value_type *a, int v, integer n; n <= 0 ==> Count(a, n, v) == 0;
|
|
*/
|
|
/*@
|
|
lemma CountHit{L}:
|
|
\forall value_type *a, int v, integer n;
|
|
0 < n ==> *(a + (n - 1)) == v ==> Count(a, n, v) == Count(a, n - 1, v) + 1;
|
|
*/
|
|
/*@
|
|
lemma CountMiss{L}:
|
|
\forall value_type *a, int v, integer n;
|
|
0 < n ==> *(a + (n - 1)) != v ==> Count(a, n, v) == Count(a, n - 1, v);
|
|
*/
|
|
/*@
|
|
lemma CountRead{L1, L2}:
|
|
\forall value_type *a, int v, integer n;
|
|
Unchanged{L1, L2}(a, n) ==> Count{L1}(a, n, v) == Count{L2}(a, n, v);
|
|
*/
|
|
/*@
|
|
predicate MultisetUnchanged{L1, L2}
|
|
(value_type *a, integer first, integer last) =
|
|
\forall int v; Count{L1}(a, first, last, v) == Count{L2}(a, first, last, v);
|
|
*/
|
|
/*@
|
|
predicate MultisetUnchanged{L1, L2}(value_type *a, integer n) =
|
|
MultisetUnchanged{L1, L2}(a, 0, n);
|
|
*/
|
|
unsigned short random_seed[3];
|
|
|
|
void random_shuffle(value_type *a, size_type n);
|
|
|
|
/*@
|
|
lemma CountSectionOne{L}:
|
|
\forall value_type *a, int v, integer m, integer n;
|
|
m <= n ==>
|
|
Count(a, m, n + 1, v) == Count(a, m, n, v) + Count(a, n, n + 1, v);
|
|
*/
|
|
/*@
|
|
lemma CountSectionUnion{L}:
|
|
\forall value_type *a, int v, integer k, integer m, integer n;
|
|
0 <= k <= m <= n ==>
|
|
Count(a, k, n, v) == Count(a, k, m, v) + Count(a, m, n, v);
|
|
*/
|
|
/*@
|
|
lemma CountOne{L}:
|
|
\forall value_type *a, int v, integer n;
|
|
0 <= n ==> Count(a, n + 1, v) == Count(a, n, v) + Count(a, n, n + 1, v);
|
|
*/
|
|
/*@
|
|
lemma CountUnion{L}:
|
|
\forall value_type *a, int v, integer m, integer n;
|
|
0 <= m <= n ==> Count(a, n, v) == Count(a, 0, m, v) + Count(a, m, n, v);
|
|
*/
|
|
size_type random_number(size_type n);
|
|
|
|
/*@
|
|
lemma random_number_modulo:
|
|
\forall unsigned long long a; a % (1ull << 48) < 1ull << 48;
|
|
*/
|
|
unsigned short random_seed[3] =
|
|
{(unsigned short)0x243f, (unsigned short)0x6a88, (unsigned short)0x85a3};
|
|
/*@ ensures lower: 0 <= \result;
|
|
ensures upper: \result <= 0x7fffffff;
|
|
assigns random_seed[0 .. 2];
|
|
*/
|
|
static long my_lrand48(void)
|
|
{
|
|
unsigned long long state =
|
|
(((unsigned long long)random_seed[0] << 32) | ((unsigned long long)random_seed[1] << 16)) | (unsigned long long)random_seed[2];
|
|
state = (0x5deece66dull * state + 0xbull) % (1ull << 48);
|
|
/*@ assert lower: state < 1ull << 48; */ ;
|
|
long result = (long)(state / (1ull << 17));
|
|
/*@ assert lower: 0 <= result; */ ;
|
|
random_seed[0u] = (unsigned short)((state >> 32) & (unsigned long long)0xffff);
|
|
random_seed[1u] = (unsigned short)((state >> 16) & (unsigned long long)0xffff);
|
|
random_seed[2u] = (unsigned short)((state >> 8) & (unsigned long long)0xffff);
|
|
return result;
|
|
}
|
|
|
|
/*@ requires 0 < n;
|
|
ensures 0 <= \result < \old(n);
|
|
assigns random_seed[0 .. 2];
|
|
*/
|
|
size_type random_number(size_type n)
|
|
{
|
|
size_type __retres;
|
|
long tmp;
|
|
tmp = my_lrand48();
|
|
;
|
|
__retres = (unsigned int)(tmp % (long)n);
|
|
return __retres;
|
|
}
|
|
|
|
/*@ requires \valid(a + (0 .. n - 1));
|
|
ensures MultisetUnchanged{Old, Here}(\old(a), \old(n));
|
|
assigns *(a + (0 .. n - 1)), random_seed[0 .. 2];
|
|
*/
|
|
void random_shuffle(value_type *a, size_type n)
|
|
{
|
|
if (0u < n) {
|
|
size_type i = 1u;
|
|
/*@ loop invariant bounds: 1 <= i <= n;
|
|
loop invariant reorder: MultisetUnchanged{Pre, Here}(a, 0, i);
|
|
loop invariant unchanged: Unchanged{Pre, Here}(a, i, n);
|
|
loop assigns i, *(a + (0 .. n - 1)), random_seed[0 .. 2];
|
|
loop variant n - i;
|
|
*/
|
|
while (i < n) {
|
|
{
|
|
size_type tmp;
|
|
tmp = random_number(i);
|
|
size_type const j = tmp + 1u;
|
|
Before: /*@ ghost ; */
|
|
swap(a + j,a + i);
|
|
/*@ assert reorder: MultisetUnchanged{Before, Here}(a, 0, j); */ ;
|
|
/*@ assert reorder: Unchanged{Before, Here}(a, j + 1, i); */ ;
|
|
/*@ assert reorder: MultisetUnchanged{Before, Here}(a, j + 1, i); */ ;
|
|
}
|
|
i ++;
|
|
}
|
|
}
|
|
return;
|
|
}
|
|
|
|
|