|
/* Generated by Frama-C */
|
|
typedef int value_type;
|
|
typedef unsigned int size_type;
|
|
/*@
|
|
predicate Reverse{K, L}(value_type *a, integer n, value_type *b) =
|
|
\forall integer i;
|
|
0 <= i < n ==> \at(*(a + i),K) == \at(*(b + ((n - 1) - i)),L);
|
|
*/
|
|
/*@
|
|
predicate Reverse{K, L}
|
|
(value_type *a, integer m, integer n, value_type *b, integer p) =
|
|
Reverse{K, L}(a + m, n - m, b + p);
|
|
*/
|
|
/*@
|
|
predicate Reverse{K, L}(value_type *a, integer m, integer n, value_type *b) =
|
|
Reverse{K, L}(a, m, n, b, m);
|
|
*/
|
|
/*@
|
|
predicate Reverse{K, L}(value_type *a, integer m, integer n, integer p) =
|
|
Reverse{K, L}(a, m, n, a, p);
|
|
*/
|
|
/*@
|
|
predicate Reverse{K, L}(value_type *a, integer m, integer n) =
|
|
Reverse{K, L}(a, m, n, m);
|
|
*/
|
|
/*@ predicate Reverse{K, L}(value_type *a, integer n) = Reverse{K, L}(a, 0, n);
|
|
*/
|
|
void reverse(value_type *a, size_type n);
|
|
|
|
/*@
|
|
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);
|
|
*/
|
|
/*@ 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);
|
|
|
|
/*@ requires valid: \valid(a + (0 .. n - 1));
|
|
ensures reverse: Reverse{Old, Here}(\old(a), \old(n));
|
|
assigns *(a + (0 .. n - 1));
|
|
*/
|
|
void reverse(value_type *a, size_type n)
|
|
{
|
|
size_type const half = n / 2u;
|
|
/*@ assert half: half <= n - half; */ ;
|
|
/*@ assert half: 2 * half <= n <= 2 * half + 1; */ ;
|
|
{
|
|
size_type i = 0u;
|
|
/*@ loop invariant bound: 0 <= i <= half <= n - i;
|
|
loop invariant left: Reverse{Pre, Here}(a, 0, i, n - i);
|
|
loop invariant middle: Unchanged{Pre, Here}(a, i, n - i);
|
|
loop invariant right: Reverse{Pre, Here}(a, n - i, n, 0);
|
|
loop assigns i, *(a + (0 .. n - 1));
|
|
loop variant half - i;
|
|
*/
|
|
while (i < half) {
|
|
swap(a + i,a + ((n - 1u) - i));
|
|
i ++;
|
|
}
|
|
}
|
|
return;
|
|
}
|
|
|
|
|