ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (1184405), страница 7
Текст из файла (страница 7)
The logic function Count determines the number of occurrences of a value x inthe index range [i,...,j-1] of an array of type value_type. Note that the bounding indices1836See http://www.sgi.com/tech/stl/count.html.i and j and the return value for Count are of type integer. The reads clause specifies the setof memory locations which Count depends on (see [10, §2.6.10] for more details).The axioms Count0 and Count2 cover the base cases, i.e., when the considered index rangeis empty or of length 1, respectively).
Axiom Count1, on the other hand, deals with the composition of adjacent ranges [i,...,j-1] and [j,...,k-1]. The Lemma CountLemma is aconsequence of axiom Count1.Listing 3.21 shows our approach for a formalization of count in ACSL.12345678/*@requires IsValidRange(a, n);assigns \nothing;ensures \result == Count(a, val, 0, n);*/size_type count(const value_type* a, size_type n, value_type val);Listing 3.21: Formal specification of count3.7.2. Implementation of countListing 3.22 shows a possible implementation of count and the corresponding loop (in)variants.Note the reference to Count in the loop invariant in Line 7.
The loop invariant in Line 6 isnecessary to prove that the local variable cnt does not exceed the range of size_type.1234567891011121314size_type count(const value_type* a, size_type n, value_type val){size_type cnt = 0;/*@loop invariant 0 <= i <= n;loop invariant 0 <= cnt <= i;loop invariant cnt == Count(a, val, 0, i);loopvariant n-i;*/for (size_type i = 0; i < n; i++)if (a[i] == val)cnt++;return cnt;}Listing 3.22: Implementation of count373.8. The search AlgorithmThe search algorithm in the C++ Standard Library finds a subsequence that is identical to agiven sequence when compared element-by-element.
For our purposes we have modified thegeneric implementation 19 to that of an array of type value_type. The signature now reads:size_type search(const value_type* a, size_type m,const value_type* b, size_type n)The function search returns the first valid index i of the array a where the conditiona[i+k] == b[k] for 0 <= k < n holds. If no such index exists then search returns thelength m of the array a.3.8.1. Formal Specification of searchOur specification of search starts with introducing the predicate HasSubRange. This predicateformalizes the fact that the sequence a contains a subsequence which is identical to the sequenceb.123456/*@predicateHasSubRange{A}(value_type* a, integer m,value_type* b, integer n) =\exists size_type k; (0 <= k <= m-n) && IsEqual{A,A}(a+k, n, b);*/Listing 3.23: The predicate HasSubRangeThe ACSL specification of search is show in Listing 3.24.The behavior has match applies if the sequence a contains a subsequence, which is identicalto the sequence b.
We express this condition in Line 8 in Listing 3.24 by using the predicateHasSubRange mentioned above.Line 9 expresses that if the ranges a or b are empty, then the return value will be 0.Line 10 indicates that the return value must be in the range [0,m-n].Line 11 indicates that the sequence a contains a subsequence (from the position result), whichis identical to the sequence b.Line 12 expresses that search returns the smallest index where b can be found in a.Figure 3.25 explains, that if result is the smallest index where b[0,...,n) can be foundin a then b is not a subrange of a[0,result+n-1).The behavior no match covers the case that there is no such subsequence in sequence a, whichequals to the sequence b.
In this case, search must return the length m of the range a.19See http://www.sgi.com/tech/stl/equal.html.3812345678910111213141516171819202122/*@requires IsValidRange(a, m);requires IsValidRange(b, n);assigns \nothing;behavior has_match:assumes HasSubRange(a, m, b, n);ensures (n == 0 || m ==0) ==> \result == 0;ensures 0 <= \result <= m-n;ensures IsEqual{Here,Here}(a+\result, n, b);ensures !HasSubRange(a, \result+n-1, b, n);behavior no_match:assumes !HasSubRange(a, m, b, n);ensures \result == m;complete behaviors;disjoint behaviors;*/size_type search(const value_type* a, size_type m,const value_type* b, size_type n);Listing 3.24: Formal specification of searchresult result+1b0abb0b101...b1result+n-1...bn-1bn-1n-1Figure 3.25.: Explanation for Line 12The formula in the assumes clause (Line 8) of the behavior has match is the negation of theassumes clause of the behavior no match.
Therefore, we can express in Lines 18 and 19 thatthese two behaviors are complete and disjoint.393.8.2. Implementation of searchOur implementation of search is shown in Listing 3.26.1 size_type search(const value_type* a, size_type m,2const value_type* b, size_type n)3 {4if ((n == 0) || (m == 0))5return 0;6if (n > m) return m;7/*@8loop invariant 0 <= i <= m-n+1;9loop invariant !HasSubRange(a, n+i-1, b, n);10loopvariant m-i;11*/12for(size_type i = 0; i <= m-n; i++)13{14if (equal(a+i, n, b)) // Is there a match?15return i;16}17return m;18 }Listing 3.26: Implementation of searchThe loop invariant in Line 9 is needed for the proof of the postcondition in Lines 10–12 of thebehavior has match (see Listing 3.24).
It expresses that for each iteration the subsequence,which equals to the sequence b, is not yet found up to that iteration step.404. Maximum and Minimum AlgorithmsIn this chapter we discuss the formal specification of algorithms that compute the maximum orminimum values of their arguments. As the algorithms in Chapter 3, they also do not modify anymemory locations. The most important new feature of the algorithms in this chapter is that theycompare values using binary operators such as < and <=.Please note that in order to compare values the STL relies solely on the less than operator < orspecial function objects.20 To be precises, the operator < must be a partial order,21 which meansthat the following rules (4.1) hold.irreflexivityantisymmetrytransitivity∀x : ¬(x < x),∀x, y : x < y =⇒ ¬(y < x),∀x, y, z : x < y ∧ y < z =⇒ x < z.(4.1a)(4.1b)(4.1c)If you wish check that the operator < of our value_type22 satisfies this properties you can formulate lemmata in ACSL and verify them with Frama-C.
(see Listing 4.1)./*@lemma LessIrreflexivity:\forall value_type a; !(a < a);lemma LessAntisymmetry:\forall value_type a, b; (a < b) ==> !(b < a);lemma LessTransitivity:\forall value_type a, b, c; (a < b) && (b < c) ==> (a < c);*/Listing 4.1: Operator < defines a partial order on value_type20See http://www.sgi.com/tech/stl/LessThanComparable.html.See http://en.wikipedia.org/wiki/Partially_ordered_set22See Section 1.32141It is of course possible to specify and implement the algorithms of this chapter by only usingoperator <.
For example, a <= b can be written as !(b < a). However, for the purpose ofthis introductory document we have opted for a more user friendly representation. Listing 4.2formulates condition on the semantics of the derived operator >, <= and >=./*@lemma Greater:\forall value_type a, b; (a > b) <==> (b < a);lemma LessOrEqual:\forall value_type a, b; (a <= b) <==> !(b < a);lemma GreaterOrEqual:\forall value_type a, b; (a >= b) <==> !(a < b);*/Listing 4.2: Semantics of derived comparison operatorsWe consider in this chapter the following algorithms.max element (Section 4.1, on Page 43) returns an index to a maximum element in range. Similar to find it also returns the smallest of all possible indices.
An alternative specificationwhich relies on user-defined predicates will be introduced in Section 4.2, on Page 45).max seq (Section 4.3, on Page 47) is very similar to max element and will serve as an example of modular verification. It returns the maximum value itself rather than an index toit.min element which can be used to find the smallest element in an array (Section 4.4).424.1.
The max element AlgorithmThe max element algorithm in the C++ Standard Template Library23 searches the maximum ofa general sequence. The signature of our version of max element reads:size_type max_element(const value_type a, size_type n);The function finds the largest element in the range a[0, n). More precisely, it returns the smallestvalid index i such that1. for each index k with 0 <= k < n the condition a[k] <= a[i] holds and2. for each index k with 0 <= k < i the condition a[k] < a[i] holds.The return value of max element is n if and only if there is no maximum, which can only occurif n == 0.4.1.1. Formal Specification of max elementA formal specification of max element in ACSL is shown in Listing 4.3.1234567891011121314151617181920/*@requiresIsValidRange(a, n);assigns \nothing;behavior empty:assumes n == 0;ensures \result == 0;behavior not_empty:assumes 0 < n;ensures 0 <= \result < n;ensures \forall integer i; 0 <= i < n ==> a[i] <= a[\result];ensures \forall integer i; 0 <= i < \result ==> a[i] < a[\result];complete behaviors;disjoint behaviors;*/size_type max_element(const value_type* a, size_type n);Listing 4.3: Formal specification of max elementWe have subdivided the specification of max element into two behaviors (named empty andnot empty).
The behavior empty contains the specification for the case that the range containsno elements. The behavior not empty checks that the range has a positive length.23See http://www.sgi.com/tech/stl/max_element.html43Line 14 indicates that the returned valid index k refers to a maximum value of the array.Line 15 expresses that k is indeed the first occurrence of a maximum value in the array.The formula in the assumes clause (Line 7) of the behavior empty is the negation of the assumesclause of the behavior not empty. Therefore, we can express in Lines 17 and 18 that these twobehaviors are complete and disjoint.4.1.2. Implementation of max elementListing 4.4 shows an implementation of max element. In our description, we concentrate onthe loop annotations in the Lines 7 to 11.1 size_type max_element(const value_type* a, size_type n)2 {3if (n == 0) return 0;45size_type max = 0;6/*@7loop invariant 0 <= i <= n;8loop invariant 0 <= max < n;9loop invariant \forall integer k; 0 <= k < i==> a[k] <= a[max];10loop invariant \forall integer k; 0 <= k < max ==> a[k] < a[max];11loopvariant n-i;12*/13for (size_type i = 0; i < n; i++)14if (a[max] < a[i])15max = i;1617return max;18 }Listing 4.4: Implementation of max elementLine 8 This loop invariant is needed to prove of the postcondition in Line 12 of the behaviornot empty in Listing 4.3, and in order to prove that all pointer accesses occur with validindices.Line 9 This loop invariant is used to prove the postcondition in Line 14 of the behaviornot empty in Listing 4.3.Line 10 This loop invariant is used to prove the postcondition in Line 15 of the behaviornot empty (see Listing 4.3).444.2.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
