|
/* Generated by Frama-C */
|
|
typedef int value_type;
|
|
typedef unsigned int size_type;
|
|
/*@
|
|
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);
|
|
*/
|
|
/*@
|
|
predicate Sorted{L}(value_type *a, integer m, integer n) =
|
|
\forall integer i, integer j; m <= i < j < n ==> *(a + i) <= *(a + j);
|
|
*/
|
|
/*@ predicate Sorted{L}(value_type *a, integer n) = Sorted(a, 0, n);
|
|
*/
|
|
void selection_sort(value_type *a, size_type n);
|
|
|
|
/*@
|
|
predicate LowerBound{L}(value_type *a, integer m, integer n, value_type v) =
|
|
\forall integer i; m <= i < n ==> v <= *(a + i);
|
|
*/
|
|
/*@
|
|
predicate LowerBound{L}(value_type *a, integer n, value_type v) =
|
|
LowerBound(a, 0, n, v);
|
|
*/
|
|
/*@
|
|
predicate MinElement{L}(value_type *a, integer n, integer min) =
|
|
0 <= min < n && LowerBound(a, n, *(a + min));
|
|
*/
|
|
/*@
|
|
predicate StrictLowerBound{L}
|
|
(value_type *a, integer m, integer n, value_type v) =
|
|
\forall integer i; m <= i < n ==> v < *(a + i);
|
|
*/
|
|
/*@
|
|
predicate StrictLowerBound{L}(value_type *a, integer n, value_type v) =
|
|
StrictLowerBound(a, 0, n, v);
|
|
*/
|
|
/*@ requires valid: \valid_read(a + (0 .. n - 1));
|
|
ensures result: 0 <= \result <= \old(n);
|
|
assigns \nothing;
|
|
|
|
behavior empty:
|
|
assumes n == 0;
|
|
ensures result: \result == 0;
|
|
|
|
behavior not_empty:
|
|
assumes 0 < n;
|
|
ensures result: 0 <= \result < \old(n);
|
|
ensures min: MinElement(\old(a), \old(n), \result);
|
|
ensures strict: StrictLowerBound(\old(a), \result, *(\old(a) + \result));
|
|
|
|
complete behaviors not_empty, empty;
|
|
disjoint behaviors not_empty, empty;
|
|
*/
|
|
size_type min_element(value_type const *a, size_type 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);
|
|
|
|
/*@
|
|
predicate StrictUpperBound{L}
|
|
(value_type *a, integer m, integer n, value_type v) =
|
|
\forall integer i; m <= i < n ==> *(a + i) < v;
|
|
*/
|
|
/*@
|
|
predicate StrictUpperBound{L}(value_type *a, integer n, value_type v) =
|
|
StrictUpperBound(a, 0, n, v);
|
|
*/
|
|
/*@
|
|
predicate UpperBound{L}(value_type *a, integer m, integer n, value_type v) =
|
|
\forall integer i; m <= i < n ==> *(a + i) <= v;
|
|
*/
|
|
/*@
|
|
predicate UpperBound{L}(value_type *a, integer n, value_type v) =
|
|
UpperBound(a, 0, n, v);
|
|
*/
|
|
/*@
|
|
lemma SortedShift{L}:
|
|
\forall value_type *a, integer l, integer r;
|
|
0 <= l <= r ==> Sorted(a, l, r) ==> Sorted(a + l, r - l);
|
|
*/
|
|
/*@
|
|
lemma LowerBoundShift{L}:
|
|
\forall value_type *a, int val, integer b, integer c, integer d;
|
|
LowerBound(a + b, c, d, val) ==> LowerBound(a, c + b, d + b, val);
|
|
*/
|
|
/*@
|
|
lemma StrictLowerBoundShift{L}:
|
|
\forall value_type *a, int val, integer b, integer c, integer d;
|
|
StrictLowerBound(a + b, c, d, val) ==>
|
|
StrictLowerBound(a, c + b, d + b, val);
|
|
*/
|
|
/*@
|
|
lemma UpperBoundShift{L}:
|
|
\forall value_type *a, int val, integer b, integer c;
|
|
UpperBound(a + b, 0, c - b, val) ==> UpperBound(a, b, c, val);
|
|
*/
|
|
/*@
|
|
lemma StrictUpperBoundShift{L}:
|
|
\forall value_type *a, int val, integer b, integer c;
|
|
StrictUpperBound(a + b, 0, c - b, val) ==> StrictUpperBound(a, b, c, val);
|
|
*/
|
|
/*@
|
|
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);
|
|
*/
|
|
/*@
|
|
lemma UnchangedImpliesMultisetUnchanged{L1, L2}:
|
|
\forall value_type *a, integer k, integer n;
|
|
Unchanged{L1, L2}(a, k, n) ==> MultisetUnchanged{L1, L2}(a, k, n);
|
|
*/
|
|
/*@
|
|
lemma MultisetUnchangedUnion{L1, L2}:
|
|
\forall value_type *a, integer i, integer k, integer n;
|
|
0 <= i <= k <= n ==>
|
|
MultisetUnchanged{L1, L2}(a, i, k) ==>
|
|
MultisetUnchanged{L1, L2}(a, k, n) ==> MultisetUnchanged{L1, L2}(a, i, n);
|
|
*/
|
|
/*@
|
|
lemma MultisetUnchangedTransitive{L1, L2, L3}:
|
|
\forall value_type *a, integer n;
|
|
MultisetUnchanged{L1, L2}(a, n) ==>
|
|
MultisetUnchanged{L2, L3}(a, n) ==> MultisetUnchanged{L1, L3}(a, n);
|
|
*/
|
|
/*@
|
|
lemma SwapImpliesMultisetUnchanged{K, L}:
|
|
\forall value_type *a, integer i, integer k, integer n;
|
|
0 <= i <= k < n ==>
|
|
\at(*(a + i),K) == \at(*(a + k),L) ==>
|
|
\at(*(a + k),K) == \at(*(a + i),L) ==>
|
|
MultisetUnchanged{K, L}(a, 0, i) ==>
|
|
MultisetUnchanged{K, L}(a, i + 1, k) ==>
|
|
MultisetUnchanged{K, L}(a, k + 1, n) ==> MultisetUnchanged{K, L}(a, n);
|
|
*/
|
|
/*@ requires valid: \valid(a + (0 .. n - 1));
|
|
ensures sorted: Sorted(\old(a), \old(n));
|
|
ensures reorder: MultisetUnchanged{Old, Here}(\old(a), \old(n));
|
|
assigns *(a + (0 .. n - 1));
|
|
*/
|
|
void selection_sort(value_type *a, size_type n)
|
|
{
|
|
size_type i = 0u;
|
|
/*@ loop invariant bound: 0 <= i <= n;
|
|
loop invariant sorted: Sorted(a, i);
|
|
loop invariant sorted: 0 < i ==> LowerBound(a, i, n, *(a + (i - 1)));
|
|
loop invariant reorder: MultisetUnchanged{Pre, Here}(a, n);
|
|
loop assigns i, *(a + (0 .. n - 1));
|
|
loop variant n - i;
|
|
*/
|
|
while (i < n) {
|
|
{
|
|
size_type tmp;
|
|
tmp = min_element((value_type const *)(a + i),n - i);
|
|
size_type const sel = i + tmp;
|
|
/*@ assert reorder: i <= sel < n; */ ;
|
|
/*@ ensures reorder: *(a + i) == \old(*(a + sel));
|
|
ensures reorder: *(a + sel) == \old(*(a + i));
|
|
ensures reorder: Unchanged{Old, Here}(a, 0, i);
|
|
ensures reorder: Unchanged{Old, Here}(a, i + 1, sel);
|
|
ensures reorder: Unchanged{Old, Here}(a, sel + 1, n);
|
|
assigns *(a + sel), *(a + i);
|
|
*/
|
|
swap(a + sel,a + i);
|
|
/*@ assert reorder: MultisetUnchanged{Pre, Here}(a, n); */ ;
|
|
}
|
|
i ++;
|
|
}
|
|
return;
|
|
}
|
|
|
|
|