ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (1184405), страница 9
Текст из файла (страница 9)
Implementation of lower boundOur implementation of lower bound is shown in Listing 5.4.1234567891011121314151617181920212223242526size_type lower_bound(const value_type *a, size_type n,value_type val){size_type left = 0;size_type right = n;size_type middle = 0;/*@loop invariant 0 <= left <= right <= n;loop assigns \nothing;loop invariant \forall integer i; 0 <= i < left ==> a[i] < val;loop invariant \forall integer i; right <= i < n ==> val <= a[i];loop variant right - left;*/while (left < right){middle = left + (right - left) / 2;if (a[middle] < val)left = middle + 1;elseright = middle;}return left;}Listing 5.4: Implementation of lower boundThe loop invariants in Lines 12–13 are needed for the proof of the postconditions in Lines 8–9(see Listing 5.3).
Each iteration step narrows down the range that contains the sought-after result.The loop invariants express that for each iteration step all indices less than the temporary leftbound left contain values smaller than val and all indices not less than the temporary rightbound right contain values not smaller than val.535.2. The upper bound AlgorithmThe upper bound27 algorithm is a version of the binary search algorithm closely relatedto lower bound of Section 5.1.The signature reads:size_type upper_bound(const value_type* a, size_type n,value_type val)In contrast to the lower bound algorithm the upper bound algorithm locates the largest index i with 0 <= i <= n such that for each index k with 0 <= k < i the condition a[k] <= valholds.
That means:• If upper bound returns an index 0 <= i < n then we can be sure that val < a[i]holds. Thus, if upper bound returns 0 then we know that val is not contained in a.• If upper bound returns n then we can only be sure that for each index 0 <= i < n holdsval <= a[i].5.2.1. Formal Specification of upper boundThe ACSL specification of upper bound is shown in Listing 5.5.1 /*@2requires IsValidRange(a,n);3requires IsSorted(a,n);45assigns \nothing;67ensures 0 <= \result <= n;8ensures \forall integer k; 0 <= k < \result ==> a[k] <= val;9ensures \forall integer k; \result <= k < n ==> val < a[k];10 */11 size_type upper_bound(const value_type *a, size_type n,12value_type val);Listing 5.5: Formal specification of upper boundThe specification is quite similar to the specification of lower bound.
The difference can beseen in Lines 8–9. As we are searching for the upper bound this time, Line 8 ensures that allindices less than the returned one contain values not greater than val and Line 9 ensures that allindices not less than the returned one contain values greater than val .27See http://www.sgi.com/tech/stl/upper_bound.html.545.2.2.
Implementation of upper boundOur implementation of upper bound is shown in Listing 5.6.123456789101112131415161718192021222324252627size_type upper_bound(const value_type *a, size_type n,value_type val){size_type left = 0;size_type right = n;size_type middle = 0;/*@loop invariant 0 <= left <= right <= n;loop assigns \nothing;loop invariant \forall integer i; 0 <= i < left ==> a[i] <= val;loop invariant \forall integer i; right <= i < n ==> val < a[i];loop variant right - left;*/while (left < right){middle = left + (right - left) / 2;if (a[middle] <= val)left = middle + 1;elseright = middle;}return right;}Listing 5.6: Implementation of upper boundThe loop invariants in the Lines 13–14 are needed for the proof of the postconditions in Lines 8–9of Listing 5.5.
The loop invariants express that for each iteration step all indices less than thetemporary left bound left contain values not greater than val and all indices not less than thetemporary right bound right contain values greater than val.555.3. The binary search AlgorithmThe binary search algorithm is one of the four binary search algorithms of the STL. For ourpurposes we have modified the generic implementation28 to that of an array of type value_type.The signature now reads:bool binary_search(const value_type* a, size_type n,value_type val);Again, binary search requires that its input array is sorted in ascending order.
It will returntrue if there exists an index i in a such that a[i] == val holds.295.3.1. Formal Specification of binary searchThe ACSL specification of binary search is shown in Listing 5.7.123456789/*@requires IsValidRange(a, n);requires IsSorted(a, n);assigns \nothing;ensures \result <==> \exists integer i; 0 <= i < n && a[i] == val;*/bool binary_search(const value_type* a, size_type n, value_type val);Listing 5.7: Formal specification of binary searchNote that that we can use our previously introduced predicate HasValue (see Page 30) in Line 7of Listing 5.8. It is interesting to compare this specification with that of find in Listing 3.12.
Bothfind and binary search allow to determine whether a value is contained in an array. The factthat the C++ standard library requires that find has linear complexity whereas binary searchmust have a logarithmic complexity can currently not be expressed with ACSL.123456789/*@requires IsValidRange(a, n);requires IsSorted(a, n);assigns \nothing;ensures \result <==> HasValue(a, n, val);*/bool binary_search(const value_type* a, size_type n, value_type val);Listing 5.8: Formal specification of binary search using the HasValue predicate2829See http://www.sgi.com/tech/stl/binary_search.html.To be more precise: The C++ standard library requires that (a[i] <= val) && (val <= a[i]) holds.For our definition of value_type (see Section 1.3) this is means that val equals a[i].565.3.2.
Implementation of binary searchOur implementation of binary search is shown in Listing 5.9.12345bool binary_search(const value_type* a, size_type n, value_type val){size_type lwb = lower_bound(a, n, val);return lwb < n && a[lwb] <= val;}Listing 5.9: Implementation of binary searchbinary search first calls the lower bound function from Section 5.1.
Remember, iflower bound returns an index 0 <= lwb < n then we can be sure that val <= a[lwb]holds.576. Mutating AlgorithmsLet us now turn our attention to another class of algorithms, viz. mutating algorithms, i.e., algorithms that change one or more ranges. In Frama-C, you can explicitly specify that, e.g., entriesin an array a may be modified by a function f, by including the following assigns clause into thef’s specification:assigns a[0..length-1];The expression length-1 refers to the value of length when f is entered, see [10, Subsection 2.3.2]. Below are the seven example algorithms we will discuss next.fill (Section 6.1 on Page 60) initializes each element of an array by a given fixed value.swap (Section 6.2 on Page 62) exchanges two values.swap values (Section 6.3 on Page 64) exchanges two values within an array.swap ranges (Section 6.4 on Page 66) exchanges the contents of the arrays of equal length, element by element.
We use this example to present “modular verification”, as swap rangesreuses the verified properties of swap.copy (Section 6.5 on Page 70) copies a source array to a destination array.reverse copy and reverse (Section 6.6 on Page 72) reverse an array. Whereasreverse copy copies the result to a separate destination array, the reverse algorithmworks in place.rotate copy (Section 6.7 on Page 76) rotates a source array by m positions and copies theresults to a destination array.replace copy (Section 6.8 on Page 78) copies a source array to a destination array, but substitutes each occurrence of a given old value by a given new value.remove copy (Section 6.9 on Page 80) copies a source array to a destination array, but omitseach occurrence of a value.unique copy (Section 6.10 on Page 84) copies a source array to a destination array, but in aconsecutive group of duplicate elements only the first one is copied.iota (Section 6.11 on Page 88) writes consecutive integers into an array.
Here we have do dealwith possible integer overflows when iota is executed.596.1. The fill AlgorithmThe fill algorithm in the C++ Standard Library initializes general sequences with a particularvalue. For our purposes we have modified the generic implementation30 to that of an array of typevalue_type. The signature now reads:void fill(value_type* a, size_type n, value_type val);6.1.1.
Formal Specification of fillListing 6.1 shows the formal specification of fill in ACSL.12345678/*@requires IsValidRange(a, n);assigns a[0..n-1];ensures \forall integer i; 0 <= i < n ==> a[i] == val;*/void fill(value_type* a, size_type n, value_type val);Listing 6.1: Formal specification of fillLine 4 expresses that fill (as a mutating algorithm), may only modify the corresponding elements of a.Line 6 formalizes the postcondition that for each element of a holds a[i] == val.30See http://www.sgi.com/tech/stl/fill.html.606.1.2. Implementation of fillListing 6.2 shows an implementation of fill.
The only noteworthy elements of this implementation are the loop annotations.12345678910void fill(value_type* a, size_type n, value_type val){/*@loop invariant 0 <= i <= n;loop invariant \forall integer k; 0 <= k < i ==> a[k] == val;loopvariant n-i;/*for (size_type i = 0; i < n; i++)a[i] = val;}Listing 6.2: Implementation of fillLine 5 This loop invariant expresses that for each iteration the array is filled with the value ofval up to the index i of the iteration. This loop invariant corresponds to the postconditionin Line 6 in Listing 6.1.616.2. The swap AlgorithmThe swap algorithm31 in the C++ STL exchanges the contents of two variables. Similarly, theiter swap algorithm32 exchanges the contents referenced by two pointers.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
