|
/* Generated by Frama-C */
|
|
typedef int value_type;
|
|
typedef unsigned int size_type;
|
|
/*@
|
|
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);
|
|
*/
|
|
/*@
|
|
predicate Partition{L}(value_type *a, integer m, integer n) =
|
|
0 <= m <= n ==>
|
|
(\forall integer i, integer k; 0 <= i < m <= k < n ==> *(a + i) <= *(a + k));
|
|
*/
|
|
/*@
|
|
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);
|
|
*/
|
|
void partial_sort(value_type *a, size_type m, size_type n);
|
|
|
|
/*@ logic integer HeapLeft(integer i) = 2 * i + 1;
|
|
*/
|
|
/*@ logic integer HeapRight(integer i) = 2 * i + 2;
|
|
*/
|
|
/*@ logic integer HeapParent(integer i) = (i - 1) / 2;
|
|
*/
|
|
/*@
|
|
lemma HeapParentOfLeft:
|
|
\forall integer p; 0 <= p ==> HeapParent(HeapLeft(p)) == p;
|
|
*/
|
|
/*@
|
|
lemma HeapParentOfRight:
|
|
\forall integer p; 0 <= p ==> HeapParent(HeapRight(p)) == p;
|
|
*/
|
|
/*@
|
|
lemma HeapParentChild:
|
|
\forall integer c, integer p;
|
|
0 < c ==> HeapParent(c) == p ==> c == HeapLeft(p) || c == HeapRight(p);
|
|
*/
|
|
/*@
|
|
lemma HeapChilds:
|
|
\forall integer a, integer b;
|
|
0 < a ==>
|
|
0 < b ==>
|
|
HeapParent(a) == HeapParent(b) ==> a == b || a + 1 == b || a == b + 1;
|
|
*/
|
|
/*@
|
|
lemma HeapParentBounds: \forall integer c; 0 < c ==> 0 <= HeapParent(c) < c;
|
|
*/
|
|
/*@
|
|
lemma HeapChildBounds:
|
|
\forall integer p; 0 <= p ==> p < HeapLeft(p) < HeapRight(p);
|
|
*/
|
|
/*@
|
|
predicate IsHeap{L}(value_type *a, integer n) =
|
|
\forall integer i; 0 < i < n ==> *(a + i) <= *(a + HeapParent(i));
|
|
*/
|
|
/*@ requires valid: \valid(a + (0 .. n - 1));
|
|
ensures heap: IsHeap(\old(a), \old(n));
|
|
ensures reorder: MultisetUnchanged{Old, Here}(\old(a), \old(n));
|
|
assigns *(a + (0 .. n - 1));
|
|
*/
|
|
void make_heap(value_type *a, size_type n);
|
|
|
|
/*@
|
|
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);
|
|
*/
|
|
/*@
|
|
predicate MaxElement{L}(value_type *a, integer n, integer max) =
|
|
0 <= max < n && UpperBound(a, n, *(a + max));
|
|
*/
|
|
/*@ requires bounds: 0 < n;
|
|
requires valid: \valid(a + (0 .. n - 1));
|
|
requires heap: IsHeap(a, n);
|
|
ensures heap: IsHeap(\old(a), \old(n) - 1);
|
|
ensures result: *(\old(a) + (\old(n) - 1)) == \old(*(a + 0));
|
|
ensures max: MaxElement(\old(a), \old(n), \old(n) - 1);
|
|
ensures reorder: MultisetUnchanged{Old, Here}(\old(a), \old(n));
|
|
assigns *(a + (0 .. n - 1));
|
|
*/
|
|
void pop_heap(value_type *a, size_type n);
|
|
|
|
/*@ requires nonempty: 0 < n;
|
|
requires valid: \valid(a + (0 .. n - 1));
|
|
requires heap: IsHeap(a, n - 1);
|
|
ensures heap: IsHeap(\old(a), \old(n));
|
|
ensures reorder: MultisetUnchanged{Old, Here}(\old(a), \old(n));
|
|
assigns *(a + (0 .. n - 1));
|
|
*/
|
|
void push_heap(value_type *a, size_type n);
|
|
|
|
/*@ requires valid: \valid(a + (0 .. n - 1));
|
|
requires heap: IsHeap(a, n);
|
|
ensures sorted: Sorted(\old(a), \old(n));
|
|
ensures reorder: MultisetUnchanged{Old, Here}(\old(a), \old(n));
|
|
assigns *(a + (0 .. n - 1));
|
|
*/
|
|
void sort_heap(value_type *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 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);
|
|
*/
|
|
/*@
|
|
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 C_Division_2: \forall integer a; 0 <= a ==> 0 <= a / 2 <= a;
|
|
*/
|
|
/*@
|
|
lemma HeapMaximum{L}:
|
|
\forall value_type *a, integer n;
|
|
1 <= n ==> IsHeap(a, n) ==> MaxElement(a, n, 0);
|
|
*/
|
|
/*@
|
|
predicate HasValue{A}(value_type *a, integer m, integer n, value_type v) =
|
|
\exists integer i; m <= i < n && *(a + i) == v;
|
|
*/
|
|
/*@
|
|
predicate HasValue{A}(value_type *a, integer n, value_type v) =
|
|
HasValue(a, 0, n, v);
|
|
*/
|
|
/*@
|
|
lemma CountSectionBounds{L}:
|
|
\forall value_type *a, int v, integer m, integer n;
|
|
0 <= m <= n ==> 0 <= Count(a, m, n, v) <= n - m;
|
|
*/
|
|
/*@
|
|
lemma CountBounds{L}:
|
|
\forall value_type *a, int v, integer n; 0 <= n ==> 0 <= Count(a, n, v) <= n;
|
|
*/
|
|
/*@
|
|
lemma HasValueImpliesPositiveCount{L}:
|
|
\forall value_type *a, int v, integer m, integer n;
|
|
0 <= m < n ==> HasValue(a, m, n, v) ==> Count(a, m, n, v) > 0;
|
|
*/
|
|
/*@
|
|
lemma PositiveCountImpliesHasValue{L}:
|
|
\forall value_type *a, int v, integer m, integer n;
|
|
0 <= m < n ==> Count(a, m, n, v) > 0 ==> HasValue(a, m, n, v);
|
|
*/
|
|
/*@
|
|
lemma ReorderImpliesMatch{K, L}:
|
|
\forall value_type *a, integer i, integer n;
|
|
0 <= i < n ==>
|
|
MultisetUnchanged{K, L}(a, n) ==> HasValue{K}(a, n, \at(*(a + i),L));
|
|
*/
|
|
/*@
|
|
lemma ReorderPreservesLowerBound{K, L}:
|
|
\forall value_type *a, integer n, int v;
|
|
0 <= n ==>
|
|
MultisetUnchanged{K, L}(a, n) ==>
|
|
LowerBound{K}(a, n, v) ==> LowerBound{L}(a, n, v);
|
|
*/
|
|
/*@
|
|
lemma ReorderPreservesUpperBound{K, L}:
|
|
\forall value_type *a, integer n, int v;
|
|
0 <= n ==>
|
|
MultisetUnchanged{K, L}(a, n) ==>
|
|
UpperBound{K}(a, n, v) ==> UpperBound{L}(a, n, v);
|
|
*/
|
|
/*@
|
|
lemma PartialReorderPreservesLowerBounds{K, L}:
|
|
\forall value_type *a, integer m, integer n;
|
|
0 < m <= n ==>
|
|
(\forall integer k; 0 <= k < m ==> LowerBound{K}(a, m, n, \at(*(a + k),K))) ==>
|
|
MultisetUnchanged{K, L}(a, 0, m) ==>
|
|
Unchanged{K, L}(a, m, n) ==> LowerBound{L}(a, m, n, \at(*(a + 0),L));
|
|
*/
|
|
/*@
|
|
predicate SwappedInside{K, L}(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) && Unchanged{K, L}(a, 0, i) &&
|
|
Unchanged{K, L}(a, i + 1, k) && Unchanged{K, L}(a, k + 1, n);
|
|
*/
|
|
/*@
|
|
lemma EqualRangesPreservesCount{K, L}:
|
|
\forall value_type *a, int v, integer m, integer n, integer p;
|
|
0 <= m <= n ==>
|
|
EqualRanges{K, L}(a, m, n, p) ==>
|
|
Count{K}(a, m, n, v) == Count{L}(a, p, p + (n - m), v);
|
|
*/
|
|
/*@
|
|
lemma SwappedInsideMultisetUnchanged{K, L}:
|
|
\forall value_type *a, integer i, integer k, integer n;
|
|
SwappedInside{K, L}(a, i, k, n) ==> MultisetUnchanged{K, L}(a, i, k + 1);
|
|
*/
|
|
/*@
|
|
lemma UnchangedSection{K, L}:
|
|
\forall value_type *a, integer m, integer n, integer p, integer q;
|
|
0 <= m <= p <= q <= n ==>
|
|
Unchanged{K, L}(a, m, n) ==> Unchanged{K, L}(a, p, q);
|
|
*/
|
|
/*@
|
|
lemma SwappedInsidePreservesMultisetUnchanged{K, L, M}:
|
|
\forall value_type *a, integer i, integer k, integer n;
|
|
MultisetUnchanged{K, L}(a, k) ==>
|
|
Unchanged{K, L}(a, k, n) ==>
|
|
SwappedInside{L, M}(a, i, k, n) ==> MultisetUnchanged{K, M}(a, k + 1);
|
|
*/
|
|
/*@ requires valid: \valid(a + (0 .. n - 1));
|
|
requires split: 0 <= m <= n;
|
|
ensures sorted: Sorted(\old(a), \old(m));
|
|
ensures partition: Partition(\old(a), \old(m), \old(n));
|
|
ensures reorder: MultisetUnchanged{Old, Here}(\old(a), \old(n));
|
|
assigns *(a + (0 .. n - 1));
|
|
*/
|
|
void partial_sort(value_type *a, size_type m, size_type n)
|
|
{
|
|
if (m > 0u) {
|
|
make_heap(a,m);
|
|
/*@ assert reorder: Unchanged{Pre, Here}(a, m, n); */ ;
|
|
{
|
|
size_type i = m;
|
|
/*@ loop invariant bound: m <= i <= n;
|
|
loop invariant heap: IsHeap(a, m);
|
|
loop invariant upper: UpperBound(a, 0, m, *(a + 0));
|
|
loop invariant lower: LowerBound(a, m, i, *(a + 0));
|
|
loop invariant reorder: MultisetUnchanged{Pre, Here}(a, i);
|
|
loop invariant unchanged: Unchanged{Pre, Here}(a, i, n);
|
|
loop assigns i, *(a + (0 .. n - 1));
|
|
loop variant n - i;
|
|
*/
|
|
while (i < n) {
|
|
if (*(a + i) < *(a + 0u)) {
|
|
/*@ ensures heap: IsHeap(a, m - 1);
|
|
ensures max: *(a + (m - 1)) == \old(*(a + 0));
|
|
ensures max: MaxElement(a, m, m - 1);
|
|
ensures reorder: MultisetUnchanged{Old, Here}(a, m);
|
|
ensures unchanged: Unchanged{Old, Here}(a, m, i);
|
|
ensures unchanged: Unchanged{Old, Here}(a, m, n);
|
|
assigns *(a + (0 .. m - 1));
|
|
*/
|
|
pop_heap(a,m);
|
|
/*@ assert lower: *(a + 0) <= *(a + (m - 1)); */ ;
|
|
/*@ assert lower: *(a + i) < *(a + (m - 1)); */ ;
|
|
/*@ assert lower: LowerBound(a, m, i, *(a + (m - 1))); */ ;
|
|
/*@ assert upper: UpperBound(a, 0, m - 1, *(a + 0)); */ ;
|
|
/*@ assert upper: UpperBound(a, 0, m, *(a + (m - 1))); */ ;
|
|
/*@ assert partition: Partition(a, m, i); */ ;
|
|
/*@ assert reorder: MultisetUnchanged{Pre, Here}(a, i); */ ;
|
|
/*@ ensures swapped: SwappedInside{Old, Here}(a, m - 1, i, n);
|
|
assigns *(a + (m - 1)), *(a + i);
|
|
*/
|
|
swap((a + m) - 1u,a + i);
|
|
/*@ assert lower: *(a + (m - 1)) < *(a + i); */ ;
|
|
/*@
|
|
assert
|
|
lower:
|
|
\forall integer k; 0 <= k < m ==> LowerBound(a, m, i + 1, *(a + k));
|
|
*/
|
|
;
|
|
/*@ assert upper: UpperBound(a, 0, m - 1, *(a + 0)); */ ;
|
|
/*@ assert reorder: MultisetUnchanged{Pre, Here}(a, i + 1); */ ;
|
|
/*@ assert unchanged: Unchanged{Pre, Here}(a, i + 1, n); */ ;
|
|
/*@ ensures heap: IsHeap(a, m);
|
|
ensures reorder: MultisetUnchanged{Old, Here}(a, m);
|
|
ensures unchanged: Unchanged{Old, Here}(a, m, i + 1);
|
|
ensures unchanged: Unchanged{Old, Here}(a, i + 1, n);
|
|
assigns *(a + (0 .. m - 1));
|
|
*/
|
|
push_heap(a,m);
|
|
/*@ assert upper: UpperBound(a, 0, m, *(a + 0)); */ ;
|
|
/*@ assert lower: LowerBound(a, m, i + 1, *(a + 0)); */ ;
|
|
}
|
|
i ++;
|
|
}
|
|
}
|
|
/*@ assert partition: Partition(a, m, n); */ ;
|
|
/*@ ensures sorted: Sorted(a, m);
|
|
ensures reorder: MultisetUnchanged{Old, Here}(a, m);
|
|
ensures reorder: MultisetUnchanged{Old, Here}(a, m, n);
|
|
assigns *(a + (0 .. m - 1));
|
|
*/
|
|
sort_heap(a,m);
|
|
/*@ assert partition: Partition(a, m, n); */ ;
|
|
/*@ assert reorder: MultisetUnchanged{Pre, Here}(a, n); */ ;
|
|
}
|
|
return;
|
|
}
|
|
|
|
|