|
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);
|
|
*/
|
|
/*@
|
|
lemma UnchangedSection{K, L}:
|
|
\forall value_type *a, integer m, integer n, integer p, integer q;
|
|
m <= p <= q <= n ==>
|
|
Unchanged{K, L}(a, m, n) ==> Unchanged{K, L}(a, p, q);
|
|
*/
|
|
/*@
|
|
axiomatic AccumulateAxiomatic {
|
|
logic integer Accumulate{L}(value_type *a, integer n, integer init) =
|
|
n <= 0? init: Accumulate(a, n - 1, init) + *(a + (n - 1));
|
|
|
|
lemma AccumulateRead{K, L}:
|
|
\forall value_type *a, integer n, integer init;
|
|
Unchanged{K, L}(a, n) ==>
|
|
Accumulate{K}(a, n, init) == Accumulate{L}(a, n, init);
|
|
|
|
}
|
|
*/
|
|
/*@
|
|
axiomatic AccumulateDefaultAxiomatic {
|
|
logic integer AccumulateDefault{L}(value_type *a, integer n) =
|
|
Accumulate(a + 1, n, (value_type)*(a + 0));
|
|
|
|
lemma AccumulateDefaultRead{K, L}:
|
|
\forall value_type *a, integer n;
|
|
0 <= n ==>
|
|
Unchanged{K, L}(a, n + 1) ==>
|
|
AccumulateDefault{K}(a, n) == AccumulateDefault{L}(a, n);
|
|
|
|
}
|
|
*/
|
|
/*@
|
|
lemma AccumulateDefault0{L}:
|
|
\forall value_type *a; AccumulateDefault(a, 0) == *(a + 0);
|
|
*/
|
|
/*@
|
|
lemma AccumulateDefault1{L}:
|
|
\forall value_type *a; AccumulateDefault(a, 1) == *(a + 0) + *(a + 1);
|
|
*/
|
|
/*@
|
|
lemma AccumulateDefaultNext{L}:
|
|
\forall value_type *a, integer n;
|
|
0 <= n ==>
|
|
AccumulateDefault(a, n + 1) == AccumulateDefault(a, n) + *(a + (n + 1));
|
|
*/
|
|
/*@
|
|
predicate PartialSum{L}(value_type *a, integer n, value_type *b) =
|
|
\forall integer i; 0 <= i < n ==> *(b + i) == AccumulateDefault(a, i);
|
|
*/
|
|
/*@
|
|
predicate AccumulateDefaultBounds{L}(value_type *a, integer n) =
|
|
\forall integer i;
|
|
0 <= i < n ==> -2147483647 - 1 <= AccumulateDefault(a, i) <= 2147483647;
|
|
*/
|
|
size_type partial_sum(value_type const *a, size_type n, value_type *b);
|
|
|
|
/*@
|
|
lemma PartialSumSection{K}:
|
|
\forall value_type *a, value_type *b, integer m, integer n;
|
|
0 <= m <= n ==> PartialSum(a, n, b) ==> PartialSum(a, m, b);
|
|
*/
|
|
/*@
|
|
lemma PartialSumUnchanged{K, L}:
|
|
\forall value_type *a, value_type *b, integer n;
|
|
0 <= n ==>
|
|
PartialSum{K}(a, n, b) ==>
|
|
Unchanged{K, L}(a, n) ==>
|
|
Unchanged{K, L}(b, n) ==> PartialSum{L}(a, n, b);
|
|
*/
|
|
/*@
|
|
lemma PartialSumStep{L}:
|
|
\forall value_type *a, value_type *b, integer n;
|
|
0 <= n ==>
|
|
PartialSum(a, n, b) ==>
|
|
*(b + n) == AccumulateDefault(a, n) ==> PartialSum(a, n + 1, b);
|
|
*/
|
|
/*@
|
|
lemma PartialSumStep2{K, L}:
|
|
\forall value_type *a, value_type *b, integer n;
|
|
1 <= n ==>
|
|
PartialSum{K}(a, n, b) ==>
|
|
Unchanged{K, L}(a, n) ==>
|
|
Unchanged{K, L}(b, n) ==>
|
|
\at(*(b + n) == AccumulateDefault(a, n),L) ==> PartialSum{L}(a, n + 1, b);
|
|
*/
|
|
/*@ requires valid: \valid_read(a + (0 .. n - 1));
|
|
requires valid: \valid(b + (0 .. n - 1));
|
|
requires sep: \separated(a + (0 .. n - 1), b + (0 .. n - 1));
|
|
requires bounds: AccumulateDefaultBounds(a, n);
|
|
ensures result: \result == \old(n);
|
|
ensures partialsum: PartialSum(\old(a), \old(n), \old(b));
|
|
ensures unchanged: Unchanged{Old, Here}(\old(a), \old(n));
|
|
assigns *(b + (0 .. n - 1));
|
|
*/
|
|
size_type partial_sum(value_type const *a, size_type n, value_type *b)
|
|
{
|
|
if (0u < n) {
|
|
*(b + 0u) = *(a + 0u);
|
|
{
|
|
size_type i = 1u;
|
|
/*@ loop invariant bound: 1 <= i <= n;
|
|
loop invariant unchanged: Unchanged{Pre, Here}(a, n);
|
|
loop invariant
|
|
accumulate: *(b + (i - 1)) == AccumulateDefault(a, i - 1);
|
|
loop invariant partialsum: PartialSum(a, i, b);
|
|
loop assigns i, *(b + (1 .. n - 1));
|
|
loop variant n - i;
|
|
*/
|
|
while (i < n) {
|
|
*(b + i) = *(b + (i - 1u)) + *(a + i);
|
|
/*@ assert unchanged: *(a + i) == \at(*(a + i),LoopCurrent); */ ;
|
|
/*@ assert unchanged: Unchanged{LoopCurrent, Here}(a, i); */ ;
|
|
/*@ assert unchanged: Unchanged{LoopCurrent, Here}(b, i); */ ;
|
|
i ++;
|
|
}
|
|
}
|
|
}
|
|
return n;
|
|
}
|
|
|
|
|