ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (1184405), страница 8

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 8)

The max element Algorithm with PredicatesIn this section we present another specification of the max element algorithm. The main difference is that we employ two user defined predicate IsMaximum and IsFirstMaximum./*@predicate IsMaximum{L}(value_type* a, integer n, integer max) =!(\exists integer i; 0 <= i < n && (a[max] < a[i]));predicate IsFirstMaximum{L}(value_type* a, integer max) =\forall integer i; 0 <= i < max ==> a[i] < a[max];*/Listing 4.5: The IsMaximum and IsFirstMaximum predicatesThe new formal specification of max element in ACSL is shown in Listing 4.6.12345678910111213141516171819/*@requiresIsValidRange(a, n);assigns \nothing;behavior empty:assumes n == 0;ensures \result == 0;behavior not_empty:assumes 0 < n;ensures 0 <= \result < n;ensures IsMaximum(a, n, \result);ensures IsFirstMaximum(a, \result);complete behaviors;disjoint behaviors;*/size_type max_element(const value_type* a, size_type n);Listing 4.6: Formal specification of max element45Listing 4.7 shows implementation of max element with rewritten loop invariants.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 IsMaximum(a, i, max);10loop invariant IsFirstMaximum(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.7: Implementation of max element464.3.

The max seq AlgorithmIn this section we consider the function max seq (see Chapter 3, [9]) that is very similar to themax element function of Section 4.1. The main difference between max seq and max elementis that max seq returns the maximum value (not just the index of it). Therefore, it requires a nonempty range as an argument.Of course, max seq can easily be implemented using max element (see Listing 4.9). Moreover, using only the formal specification of max element in Listing 4.3 we are also able todeductively verify the correctness of this implementation.

Thus, we have a simple example ofmodular verification in the following sense:Any implementation of max element that is separately proven to implement thecontract in Listing 4.3 makes max seq behave correctly. Once the contracts havebeen defined, the function max element could be implemented in parallel, or justafter max seq, without affecting the verification of max seq.4.3.1. Formal Specification of max seqA formal specification of max seq in ACSL is shown in Listing 4.8.12345678910/*@requires n > 0;requires \valid(p+ (0..n-1));assigns\nothing;ensuresensures\forall integer i; 0 <= i <= n-1 ==> \result >= p[i];\exists integer e; 0 <= e <= n-1 && \result == p[e];*/value_type max_seq(const value_type* p, size_type n) ;Listing 4.8: Formal specification of max seqLines 2 express that max seq requires a non-empty range as input.Line 3 states that the block pointed to by p must contain at least n elements.

In other words,p[0], p[1], ..,p[n-1] must all be valid memory accesses. Also possible would be thealready-known notation IsValidRange(p, n).Lines 7 and 8 formalize that max seq indeed returns the maximum value of the range.474.3.2. Implementation of max seqListing 4.9 shows the trivial implementation of max seq using max element. Since max seqrequires a non-empty range the call of max element returns an index to a maximum value inthe range.241234value_type max_seq(const value_type* p, size_type n){return p[max_element(p, n)];}Listing 4.9: Implementation of max seq24The fact that max element returns the smallest index is of no importance in this context.484.4. The min element AlgorithmThe min element algorithm in the C++ standard library25 searches the minimum in a generalsequence.

The signature of our version of min element reads:size_type min_element(const value_type* a, size_type n);The function min element finds the smallest element in the range a[0,n). More precisely, itreturns the smallest valid 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 min element is n if and only if n == 0.4.4.1.

Formal Specification of min elementThe ACSL specification of min element is shown in Listing 4.10. Given the great similarity tothe max element specification (see Section 4.1) we did not provide a detailed explanation here.1234567891011121314151617181920/*@requires IsValidRange(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[\result] <= a[i];ensures \forall integer i; 0 <= i < \result ==> a[\result] < a[i];complete behaviors;disjoint behaviors;*/size_type min_element(const value_type* a, size_type n);Listing 4.10: Formal specification of min element25See http://www.sgi.com/tech/stl/min_element.html.494.4.2.

Implementation of min elementListing 4.11 shows the implementation of min element. Given the great similarity with respectto the max element implementation (see Section 4.1) we did not provide a detailed explanationhere.1 size_type min_element(const value_type* a, size_type n)2 {3if (0 == n) return n;45size_type min = 0;6/*@7loop invariant 0 <= i<= n;8loop invariant 0 <= min < n;9loop invariant \forall integer k; 0 <= k < i==> a[min] <= a[k];10loop invariant \forall integer k; 0 <= k < min ==> a[min] < a[k];11loopvariant n-i;12*/13for (size_type i = 0; i < n; i++)14if (a[i] < a[min])15min = i;1617return min;18 }Listing 4.11: Implementation of min element505.

Binary Search AlgorithmsIn this chapter, we consider three of the four binary search algorithms of the STL, namely• lower bound in Section 5.1,• upper bound in Section 5.2 and• binary search in Section 5.3.All binary search algorithms require that their input array is sorted in ascending order. The predicate IsSorted in Listing 5.1 formalizes these requirements./*@predicate IsSorted{L}(value_type* a, integer n) =\forall integer i, j; 0 <= i < j < n ==> a[i] <= a[j];*/Listing 5.1: The predicate IsSortedAs in the case of the of maximum/minimum algorithms from Chapter 4 the binary search algorithms only use the less-than operator < (and the derived operators <=, > and >=) to determinewhether a particular a particular value is contained in a sorted range. Thus, different to the findalgorithm in Section 3.3, the equality operator == does not occur directly in the specification ofbinary search.We found that the formal verification of the binary search algorithms poses some challenges toautomatic theorem provers.

We were able to overcome these difficulties by explicitly stating asimple fact on integer division (see Listing 5.2).123456789/*@axiomatic Division{predicate NonNegative(integer i) = (0 <= i);axiom div:\forall integer i; NonNegative(i) ==> 0 <= 2*(i/2) <= i;}*/Listing 5.2: Axiomatic Description of Division515.1. The lower bound AlgorithmThe lower bound algorithm is one of the four binary search algorithms of the STL.

For ourpurposes we have modified the generic implementation26 to that of an array of type value_type.The signature now reads:size_type lower_bound(const value_type* a, size_type n,value_type val);As with the other binary search algorithms lower bound requires that its input array is sorted inascending order. Specifically, lower bound will return the largest index i with 0 <= i <= nsuch that for each index k with 0 <= k < i the condition a[k] < val holds. This specificationmakes lower bound a bit tricky to use as a search algorithm:• If lower bound returns n then for each index 0 <= i < n holds a[i] < val. Thus,val is not contained in a.• If, however, lower bound returns an index 0 <= i < n then we can only be sure thatval <= a[i] holds.5.1.1. Formal Specification of lower boundThe ACSL specification of lower bound is shown in Listing 5.3.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 lower_bound(const value_type* a, size_typen,12value_type val);Listing 5.3: Formal specification of lower boundLine 3 formalizes the requirement that the values in the array need to be sorted in an ascendingorder by using the predicate IsSorted.Lines 7–9 formalize the central requirements on the return value of lower bound.26See http://www.sgi.com/tech/stl/lower_bound.html.525.1.2.

Характеристики

Список файлов книги