ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (1184405), страница 11
Текст из файла (страница 11)
However, this ACSLfeature is not jet supported by Jessie. To tell Frama-C that the arrays a and b must notoverlap, we used pragmas cf. the discussion under 6.4.1 on Page 66 sqq. and Section 1.4 onPage 10.Line 6 The copy algorithm assigns the elements from the source range a to the destination rangeb, modifying the memory of the elements pointed to by b. Nothing else must be altered.Line 8 ensures that the contents of a were actually copied to b. Again, we can use the IsEqualpredicate from Section 3.1 to express that the array a equals b after copy has been called.34See http://www.sgi.com/tech/stl/copy.html.706.5.2.
Implementation of copyListing 6.12 shows an implementation of the copy function.12345678910111213void copy(const value_type* a, size_type n, value_type* b){/*@loop invariant 0 <= i <= n;loop assigns b[0..i-1];loop invariant IsEqual{Here,Here}(a, i, b);loopvariant n-i;*/for (size_type i = 0; i < n; i++)b[i] = a[i];}Listing 6.12: Implementation of copyHere are some remarks on its loop invariants.Line 6 The assigns clause ensures that nothing, but the range b[0..i-1] is modified.Line 8 For the postcondition to be true, we must ensure that for every element i, the comparisona[i] == b[i] is true.
This can be expressed by using the IsEqual predicate. Thisloop invariant is necessary to prove the postcondition in Line 8 in Listing 6.11.716.6. The reverse copy and reverse algorithmsThe reverse copy35 and reverse36 algorithms of the C++ Standard Library invert the orderof elements in a sequence. Whereas reverse copy does not change the input sequence andcopies its result to the output sequence, the reverse algorithm works in place.For our purposes we have modified the generic implementations to that of a range of type value_type.The signatures now reads:void reverse_copy(const value_type* a, size_type n, value_type* b);void reverse(value_type* a, size_type n);First we will take a look at the formal specification and implementation of reverse copy.6.6.1. Formal Specification of reverse copyInformally, reverse copy copies the elements from the array a into array b such that the copyis a reverse of the original array.
Thus, after calling reverse copy the following conditionsshall be satisfied.b[0]b[1]...====...a[n-1]a[n-2]...b[n-1]==a[ 0 ]The ACSL specification of reverse_copy is shown in Listing 6.13.123456789/*@requires IsValidRange(a, n);requires IsValidRange(b, n);assigns b[0..(n-1)];ensures \forall integer i; 0 <= i < n ==> b[i] == a[n-1-i];*/void reverse_copy(const value_type* a, size_type n, value_type* b);Listing 6.13: Formal specification of reverse_copyLine 7 ensures that the contents of a were actually copied reversely to b.3536See http://www.sgi.com/tech/stl/reverse_copy.html.See http://www.sgi.com/tech/stl/reverse_copy.html.726.6.2.
Implementation of reverse copyListing 6.14 shows an implementation of the reverse_copy function.1234567891011void reverse_copy(const value_type* a, size_type n, value_type* b){/*@loop invariant 0 <= i <= n;loop invariant \forall integer k; 0 <= k < i ==>b[k] == a[n-1-k];loop variant n-i;*/for(size_type i = 0; i < n; i++)b[i] = a[n-1-i];}Listing 6.14: Implementation of reverse_copyFor the postcondition to be true, we must ensure that for every element i, the comparisonb[i] == a[n-1-i] is true.
This is formalized by the loop invariant in Lines 5–6. You can seethat it is nearly similar to the postcondition in Line 7 in Listing 6.13. To verify reverse we willneed some more loop invariants.736.6.3. Formal Specification of reverseThe ACSL specification for the reverse function is shown in listing 6.15.123456789/*@requires IsValidRange(a, n);assigns a[0..(n-1)];ensures \forall integer i; 0 <= i < n ==>a[i] == \old(a[n-1-i]);*/void reverse(value_type* a, size_type n);Listing 6.15: Formal specification of reverseLines 6–7 ensure that the contents of a were actually reversed.
Compare with Line 7 in listing 6.13where we make the same comparison but with array b.6.6.4. Implementation of reverseListing 6.16 shows an implementation of the reverse function.Here are some remarks on its loop invariants.Line 12 The indices first and last are used to point at the elements which will be swapped inthe current loop cycle. Therefore it is important that decreasing of last and increasing offirst happen at the same time. Thus, the sum of the two indices is constant. By that andthe initialization of both indices we can ensure that the right elements will be swapped.Lines 14–15 expresses that the sequence from position 0 up to but not including first is alreadythe reversed end part of a.Lines 17–18 formalize that the sequence which goes from the position after last until n-1is already reversed.
This loop invariant together with the one above corresponds to thepostcondition in Lines 6–7 in Listing 6.15.For the implementation at Line 27, we use the swap values function instead of swap. Bothfunctions swap two elements, but swap values also ensures that all the other elements of anarray are unchanged, see Section 6.3 on Page 64. This stronger formal specification is necessaryto verify reverse.74123456789101112131415161718192021222324252627282930void reverse(value_type* a, size_type n){if (n > 0) // needed to prove absence of overflow with Simplify{// when the variable ’last’ is initializedsize_type first = 0;size_type last = n-1;/*@loop invariant 0 <= first;loop invariant last < n;loop invariant first + last == n - 1;loop invariant \forall integer k;0 <= k < first ==> a[k] == \at(a[n-1-k], Pre);loop invariant \forall integer k;last < k < n==> a[k] == \at(a[n-1-k], Pre);loop assigns a[0..(first-1)];loop assigns a[(last+1)..(n-1)];loopvariant last;*/while (first < last){swap_values(a, n, first++, last--);}}}Listing 6.16: Implementation of reverse756.7.
The rotate copy AlgorithmThe rotate copy algorithm in the C++ Standard Library rotates a sequence by m positions andcopies the results to another same sized sequence. For our purposes we have modified the genericimplementation37 to that of a range of type value_type. The signature now reads:void rotate_copy(const value_type* a, size_type m,size_type n, value_type* b);Informally, the function copies the elements from the array a into array b such that the copy is arotated version of the original array. In other words: After calling rotate copy the followingconditions shall be satisfied.b[0]b[1]...====...a[m]a[m+1]...b[n-m-1]==a[n-1]b[n-m]b[n-m+1]...====...a[0]a[1]...b[n-1]==a[m-1]This function refers to the previously discussed algorithm copy.
Thus, rotate copy servesas another example for “modular verification”. The specification of copy will be automaticallyintegrated into the proof of rotate copy.37See http://www.sgi.com/tech/stl/rotate_copy.html.766.7.1. Formal Specification of rotate copyThe ACSL specification of rotate_copy is shown in Listing 6.17.12345678910111213/*@requires IsValidRange(a, n);requires IsValidRange(b, n);//requires \separated(a+(0..n-1), b+(0..n-1));requires 0 <= m <= n;assigns b[0..(n-1)];ensures IsEqual{Here,Here}(a, m, b+(n-m));ensures IsEqual{Here,Here}(a+m, n-m, b);*/void rotate_copy(const value_type* a, size_type m, size_type n,value_type* b);Listing 6.17: Formal specification of rotate_copyLine 4 The separated-clause tells Frama-C that a and b must not overlap.Line 5 guarantees the range of the variable m.Line 7 The rotate copy algorithm assigns the elements in the range b, modifying the memoryof the elements pointed to by b.
Nothing else must be altered.6.7.2. Implementation of rotate copyListing 6.18 shows an implementation of the rotate_copy function. In the rotate_copy function, we simply call the function copy twice.123456void rotate_copy(const value_type* a, size_type m, size_type n,value_type* b){copy(a, m, b+(n-m));copy(a+m, n-m, b);}Listing 6.18: Implementation of rotate_copy776.8. The replace copy AlgorithmThe replace copy algorithm of the C++ Standard Library substitutes specific elements fromgeneral sequences. Here, the general implementation38 has been altered to process value_typeranges. The new signature reads:size_type replace_copy(const value_type* a, size_type n,value_type* b,value_type old_val, value_type new_val);replace_copy copies the elements from the range a[0..n] to range b[0..n], substitutingevery occurrence of old_val by new_val.
The return value is the length of the range. As thelength of the range is already a parameter of the function this return value does not contain newinformation. However, the length returned is analogous to the implementation of the C++ StandardLibrary. Again, we need to issue appropriate command-line options to tell Frama-C that the rangesa and b must not overlap, cf.
the discussion under 6.4.1 on Page 66 f. and Section 1.4 on Page 10.6.8.1. Formal Specification of replace copyThe ACSL specification of replace_copy is shown in Listing 6.19.1 /*@2requires IsValidRange(a, n);3requires IsValidRange(b, n);45assigns b[0..n-1];67ensures \forall integer j; 0 <= j < n ==>8(a[j] == old_val && b[j] == new_val) ||9(a[j] != old_val && b[j] == a[j]);10ensures \result == n;11 */12 size_type replace_copy(const value_type* a, size_type n,13value_type* b,14value_type old_val, value_type new_val);Listing 6.19: Formal specification of the replace_copy functionLines 7–9 For every element a[j] of a, we have two possibilities.
Either it equals old_val orit is different from old_val. In the former case, we specify that the corresponding elementb[j] has to be substituted with new_val. In the latter case, we specify that b[j] must bea[j]. Instead of Lines 8–9, we could just as well have specified(a[j] == old_val ==> b[j] == new_val) &&(a[j] != old_val ==> b[j] == a[j]);because the formulae p && q || !p && r and (p ==> q) && (!p ==> r) arelogically equivalent.38See http://www.sgi.com/tech/stl/replace_copy.html.78Line 10 formalizes that the returned value is equal to the length of the range.6.8.2. Implementation of replace copyAn implementation (including loop annotations) of replace_copy is shown in Listing 6.20.12345678910111213141516171819size_type replace_copy(const value_type* a, size_type n,value_type* b,value_type old_val, value_type new_val){/*@loop invariant 0 <= i <= n;loop assigns b[0..i-1];loop invariant \forall integer j; 0(a[j] == old_val &&(a[j] != old_val &&loopvariant n-i;*/for (size_type i = 0; i < n; i++)b[i] = (a[i] == old_val ? new_val :<= j < i ==>b[j] == new_val) ||b[j] == a[j]);a[i]);return n;}Listing 6.20: Implementation of the replace_copy functionLines 10–12 are necessary to prove the Lines 7–9 of the postcondition in Listing 6.19.796.9.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
