ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (1184405), страница 6
Текст из файла (страница 6)
We express thiscondition by the formula in Line 7 in Listing 3.9.14See http://www.sgi.com/tech/stl/find.html.28Line 8 expresses that if the assumptions of the behavior are satisfied then find will return a validindex.Line 9 indicates that for the returned (valid) index i, a[i] == val holds.Line 10 is important because it expresses that find returns the smallest index i for whicha[i] == val holds.The behavior none covers the case that the sought-after value is not contained in the array (seeLine 13 in Listing 3.9). In this case, find must return the length n of the range a (see Line 14).The formula in the assumes clause (Line 7) of the behavior some is the negation of the assumesclause of the behavior none.
Therefore, we can express in Lines 16 and 17 that these two behaviors are complete and disjoint.3.3.2. Implementation of findListing 3.10 shows a straightforward implementation of find. The only noteworthy elements ofthis implementation are the three loop annotations in Lines 4 to 6.12345678910111213size_type find(const 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++)if (a[i] == val)return i;return n;}Listing 3.10: Implementation of findLine 4 This loop invariant is needed to prove that accesses to a only occur with valid indices.Line 5 This loop invariant is needed for the proof of the postconditions in Lines 8–10 of thebehavior some (see Listing 3.9).
It expresses that for each iteration the sought-after valueis not yet found up to that iteration step.Line 6 This loop variant is needed to generate correct verification conditions for the terminationof the loop.293.4. The find Algorithm ReconsideredIn this section we specify the find algorithm in a slightly different way when compared to Section 3.3. Our approach is motivated by a considerable amount of closely related formulas.
Wehave in Listings 3.9 and 3.10 the following formulas\exists\forall\forall\forallintegerintegerintegerintegeri;i;i;k;0000<=<=<=<=iiik<<<<n && a[i] == val;\result ==> a[i] != val;n ==> a[i] != val;i ==> a[k] != val;Note that the first formula is the negation of the third one.In order to be more explicit about the commonalities of these formulas we define a predicate,called HasValue (see Listing 3.11), which describes the situation that there is a valid index isuch thata[i] == valholds.12345/*@predicateHasValue{A}(value_type* a, integer n, value_type val) =\exists integer i; 0 <= i < n && a[i] == val;/*Listing 3.11: The predicate HasValueWith this predicate we can encapsulate all uses of the ∀ and ∃ quantifiers in both the specificationof the function contract of find and in the loop annotations. The result is shown in Listings 3.12and 3.13.3.4.1.
Formal Specification of findThis approach leads to a specification of find that is more readable than the one described inSection 3.3.In particular, it can be seen immediately that the conditions in the assume clauses of the twobehaviors some and none are mutually exclusive since one is the negation of the other.
Moreover,the requirement that find returns the smallest index can also be expressed using the HasValuepredicate, as depicted in Line 10 in Listing 3.12.3012345678910111213141516171819/*@requiresassignsIsValidRange(a, n);\nothing;behavior some:assumes HasValue(a, n, val);ensures 0 <= \result < n;ensures a[\result] == val;ensures !HasValue(a, \result, val);behavior none:assumes !HasValue(a, n, val);ensures \result == n;complete behaviors;disjoint behaviors;*/size_type find(const value_type* a, size_type n, value_type val);Listing 3.12: Formal specification of find using the HasValue predicate3.4.2. Implementation of findThe predicate HasValue is also used in the loop annotation inside the implementation of find(see Line 5 in Listing 3.13).12345678910111213size_type find(const value_type* a, size_type n, value_type val){/*@loop invariant 0 <= i <= n;loop invariant !HasValue(a, i, val);loopvariant n-i;*/for (size_type i = 0; i < n; i++)if (a[i] == val)return i;return n;}Listing 3.13: Implementation of find with loop annotations based on HasValue313.5.
The find first of AlgorithmThe find first of algorithm15 is closely related to find (see Sections 3.3 and 3.4).size_type find_first_of(const value_type* a, size_type m,const value_type* b, size_type n);As in find it performs a sequential search. However, whereas find searches for a particularvalue, find first of returns the least index i such that a[i] is equal to one of the valuesb[0], . . ., b[n-1].3.5.1.
Formal Specification of find first ofSimilar to our approach in Section 3.4, we define a predicate HasValueOf that formalizes thefact that there are valid indices i for a and j of b such that a[i] == b[j] hold. One way toachieve this would be to define HasValueOf as follows:/*@predicateHasValueOf{A}(value_type*value_type*\exists integer i, j; 00*/a,b,<=<=integer m,integer n) =i < m &&j < n && a[i] == b[j];However, we have chosen to reuse the predicateHasValue (Listing 3.11) to define the HasValueOf predicate. The result is shown in Listing 3.14.1234567/*@predicateHasValueOf{A}(value_type* a, integer m,value_type* b, integer n) =\exists integer i; 0 <= i < m &&HasValue{A}(b, n, \at(a[i],A));*/Listing 3.14: The predicate HasValueOfBoth the predicates HasValueOf and HasValue occur in the formal specification offind first of (see Listing 3.15).
Note how similar the specification offind first of becomes to that of find (Listing 3.12) when using these predicates.3.5.2. Implementation of find first ofOur implementation of find first of is shown in Listing 3.16.15See http://www.sgi.com/tech/stl/find_first_of.html.32123456789101112131415161718192021/*@requires IsValidRange(a, m);requires IsValidRange(b, n);assigns \nothing;behavior found:assumes HasValueOf(a, m, b, n);ensures 0 <= \result < m;ensures HasValue(b, n, a[\result]);ensures !HasValueOf(a, \result, b, n);behavior not_found:assumes !HasValueOf(a, m, b, n);ensures \result == m;complete behaviors;disjoint behaviors;*/size_type find_first_of(const value_type* a, size_type m,const value_type* b, size_type n);Listing 3.15: Formal specification of find first of1234567891011121314size_type find_first_of (const value_type* a, size_type m,const value_type* b, size_type n){/*@loop invariant 0 <= i <= m;loop invariant !HasValueOf(a, i, b, n);loopvariant m-i;*/for (size_type i = 0; i < m; i++)if (find(b, n, a[i]) < n)return i;return m;}Listing 3.16: Implementation of find first ofNote the call of the find function in Line 10 above.
In the original STL implementation16 ,find first of does not call find but rather inlines it. The reason for this were probablyefficiency considerations. We opted for an implementation of find first of that emphasizesreuse. We also think that inlining the call to find by a compiler can address the performance considerations mentioned above. Besides, leading to a more concise implementation, it also enablesus to save time in writing additional loop annotations.16See http://www.sgi.com/tech/stl/stl_algo.h333.6. The adjacent find AlgorithmThe adjacent find algorithm17size_type adjacent_find(const value_type* a, size_type n);returns the smallest valid index i, such that i+1 is also a valid index and such thata[i] == a[i+1]holds. The adjacent find algorithm returns n if no such index exists.3.6.1.
Formal Specification of adjacent findAs in the case of other search algorithms, we first define a predicate HasEqualNeighbors (seeListing 3.17) that captures the essence of finding two adjacent indices at which the array holdsequal values.12345/*@predicateHasEqualNeighbors{A}(value_type* a, integer n) =\exists integer i; 0 <= i < n-1 && a[i] == a[i+1];/*Listing 3.17: The predicate HasEqualNeighbors1 /*@2requires IsValidRange(a, n);34assigns \nothing;56behavior some:7assumes HasEqualNeighbors(a, n);8ensures 0 <= \result < n-1;9ensures a[\result] == a[\result+1];10ensures !HasEqualNeighbors(a, \result);1112behavior none:13assumes !HasEqualNeighbors(a, n);14ensures \result == n;1516complete behaviors;17disjoint behaviors;18 */19 size_type adjacent_find(const value_type* a, size_type n);Listing 3.18: Formal specification of adjacent find1734See http://www.sgi.com/tech/stl/adjacent_find.htmlWe use the predicate HasEqualNeighbors in Lines 7, 10 and 13 of the formal specification ofadjacent find (see Listing 3.18).3.6.2.
Implementation of adjacent findThe implementation of adjacent find, including loop (in)variants is shown in Listing 3.19.Please note the use of the predicate HasEqualNeighbors in loop invariant in Line 7.123456789101112131415size_type adjacent_find(const value_type* a, size_type n){if (0 == n) return n;/*@loop invariant 0 <= i < n;loop invariant !HasEqualNeighbors(a, i+1);loopvariant n-i;*/for (size_type i = 0; i < n-1; i++)if (a[i] == a[i+1])return i;return n;}Listing 3.19: Implementation of adjacent find353.7.
The count AlgorithmThe count algorithm in the C++ standard library counts the frequency of occurrences for a particular element in a sequence. For our purposes we have modified the generic implementation18 tothat of arrays of type value_type. The signature now reads:size_type count(const value_type* a, size_type n, value_type val);Informally, the function returns the number of occurrences of val in the array a.3.7.1. Formal Specification of countThe specification of count will be fairly short because it employs the logic function Countwhose considerably longer definition is given in Listing 3.20. This definition of Count is ageneralization of the logic function nb_occ of the ACSL specification [10, p.50].1 /*@2axiomatic CountAxiomatic3{4logic integer Count{L}(value_type* a, value_type v,5integer i, integer j) reads a[i..(j-1)];67axiom Count0:8\forall value_type *a, v, integer i;9Count(a, v, i, i) == 0;1011axiom Count1:12\forall value_type *a, v, integer i, j, k;130 <= i <= j <= k ==> Count(a, v, i ,k) ==14Count(a, v, i, j) + Count(a, v, j, k);1516axiom Count2:17\forall value_type *a, v, integer i;18(a[i] != v ==> Count(a, v, i, i+1) == 0) &&19(a[i] == v ==> Count(a, v, i, i+1) == 1);20}2122lemma CountLemma: \forall value_type *a, v, integer i;230 <= i ==> Count(a, v, 0, i+1) ==24Count(a, v, 0, i) + Count(a, v, i, i+1);25 */Listing 3.20: Axiomatic definition of CountThe ACSL keyword in Line 2 axiomatic is used to gather the logic function Count and itsdefining axioms.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
