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

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

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

The IsEqual PredicateThe fact that two arrays a[0],...,a[n-1] and b[0],...,b[n-1] are equal when comparedelement by element, is a property we might need again in other specifications, as it describes avery basic behavior.The motto don’t repeat yourself is not just good programming practice.9 It is also true for conciseand easy to understand specifications.

We will therefore introduce specification elements that wecan apply to the equal algorithm as well as to other specifications and implementations with thedescribed behavior.In Listing 3.2 we introduce the predicate IsEqual.123456/*@predicateIsEqual{A,B}(value_type* a, integer n, value_type* b) =\forall integer i; 0 <= i < n ==>\at(a[i], A) == \at(b[i], B);*/Listing 3.2: The predicate IsEqualThis predicate formalizes the fact that the arrays a[0],...,a[n-1] and b[0],...,b[n-1]are equal when compared element by element. The letters A and B are labels10 that must besupplied when using the predicate IsEqual. We use labels in the definition of IsEqual toextend its applicability. The expression \at(a[i], A) means that a[i] is evaluated at thelabel A. Frama-C defines several standard labels, e.g.

Old and Post, a programmer can useto refer to the pre-state or post-state, respectively, of a function. For more details on labels werefer to the ACSL specification [10, p. 39].910Compare http://en.wikipedia.org/wiki/Don’t_repeat_yourself.Labels are used in C to name the target of the goto jump statement.23Using this predicate we can reformulate the specification of equal from Listing 3.1 as shownin Listing 3.3. Here we use the predefined label Here. When used in an assumes clause thelabel Here refers to the pre-state of a function.123456789/*@requires IsValidRange(a, n);requires IsValidRange(b, n);assigns \nothing;ensures \result <==> IsEqual{Here,Here}(a, n, b);*/bool equal(const value_type* a, size_type n, const value_type* b);Listing 3.3: Formal specification of equal using the IsEqual predicate3.1.3.

Implementation of equalListing 3.4 shows one way to implement the function equal. In our description, we concentrateon the loop annotations in Lines 4 to 6.1 bool equal(const value_type* a, size_type n, const value_type* b)2 {3/*@4loop invariant 0 <= i <= n;5loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k];6loopvariant n-i;7/*8for (size_type i = 0; i < n; i++)9if (a[i] != b[i])10return false;1112return true;13 }Listing 3.4: Implementation of equalLine 4 This loop invariant is needed to prove that all accesses to a and b occur with valid indices.However, we may not require simplyloop invariant 0 <= i < n;since the very last loop iteration would violate this formula. Therefor, we have to weakenthe formula to that shown in Line 4 of Listing 3.4, which is preserved by all iterations of theloop.

Note that 0 <= i < n is still valid immediately before the array accesses in Line 9,since we may assume there in addition that the loop condition i < n holds. However,0 <= i < n is invalid after completion of the loop, while the loop invariant is guaranteedto hold there, too, cf. the loop rule in Figure 2.11 on Page 17.24Line 5 This loop invariant is needed to prove that for each iteration all elements of a and b up tothat iteration step are equal.Line 6 This loop variant is needed to generate correct verification conditions for the terminationof the for- loop that starts in Line 8. In order to prove the termination of the loop, Frama-Cneeds to know an expression whose value is decreased by each and every loop cycle and isalways positive11 [10, Subsections 2.4.2, 2.5.1].

For a for loop as simple as that in Line8–10, the expression n-i is sufficient for that purpose.Again, we can use the predicate IsEqual in order to simplify the loop invariant in Line 5. Listing 3.5 shows the modified implementation using the predicate IsEqual.12345678910111213bool equal(const value_type* a, size_type n, const value_type* b){/*@loop invariant 0 <= i <= n;loop invariant IsEqual{Here,Here}(a, i, b);loopvariant n-i;/*for (size_type i = 0; i < n; i++)if (a[i] != b[i])return false;return true;}Listing 3.5: Implementation of equal using the IsEqual predicate11Except for possibly the very last iteration.253.2.

The mismatch AlgorithmThe mismatch algorithm is closely related to the negation of equal from Section 3.1. Itssignature readssize_type mismatch(const value_type* a, int n,const value_type* b);The function mismatch returns the smallest index where the two ranges a and b differ. If nosuch index exists, that is, if both ranges are equal then mismatch returns the length n of the tworanges.123.2.1. Formal Specification of mismatchWe use the IsEqual predicate also for the formal specification of mismatch that is shown inListing 3.6.Note in particular the use of IsEqual in Line 15 of Listing 3.6 in order to express that mismatchreturns the smallest index where the two arrays differ.

Note also that the completeness and disjointness of the behaviors all_equal and some_not_equal has now become immediately obvious,since their assumes clauses are just literal negations of each other.1 /*@2requires IsValidRange(a, n);3requires IsValidRange(b, n);45assigns \nothing;67behavior all_equal:8assumes IsEqual{Here,Here}(a, n, b);9ensures \result == n;1011behavior some_not_equal:12assumes !IsEqual{Here,Here}(a, n, b);13ensures 0 <= \result < n;14ensures a[\result] != b[\result];15ensures IsEqual{Here,Here}(a, \result, b);1617complete behaviors;18disjoint behaviors;19 */20 size_type mismatch(const value_type* a, size_type n,21const value_type* b);Listing 3.6: Formal specification of mismatch12See also http://www.sgi.com/tech/stl/mismatch.html.263.2.2. Implementation of mismatchListing 3.7 shows an implementation of mismatch that we have enriched with some loop annotations to support the deductive verification of the specification given in Listing 3.6.1234567891011121314size_type mismatch(const value_type* a, size_type n,const value_type* b){/*@loop invariant 0 <= i <= n;loop invariant IsEqual{Here,Here}(a, i, b);loopvariant n-i;/*for (size_type i = 0; i < n; i++)if (a[i] != b[i])return i;return n;}Listing 3.7: Implementation of mismatchWe use the predicate IsEqual in Line 6 of Listing 3.7 in order to express that all indices k thatare less than the current index i satisfy the condition a[k] == b[k].

This is necessary to provethat mismatch indeed returns the smallest index where the two ranges differ.3.2.3. Implementation of equal by calling mismatchListing 3.8 shows an implementation of the equal algorithm by a simple call of mismatch.131234bool equal(const value_type* a, size_type n, const value_type* b){return mismatch(a, n, b) == n;}Listing 3.8: Implementation of equal with mismatch13See also the note on the relationship of equal and mismatch on http://www.sgi.com/tech/stl/equal.html.273.3.

The find AlgorithmThe find algorithm in the C++ standard library implements sequential search for general sequences.14 We have modified the generic implementation, which relies heavily on C++ templates,to that of a range of type value_type. The signature now reads:size_type find(const value_type* a, size_type n, value_type val);The function find returns the least valid index i of a where the conditiona[i] == valholds.

If no such index exists then find returns the length n of the array.3.3.1. Formal Specification of findThe formal specification of find in ACSL is shown in Listing 3.9.1 /*@2requires IsValidRange(a, n);34assigns \nothing;56behavior some:7assumes \exists integer i; 0 <= i < n && a[i] == val;8ensures 0 <= \result < n;9ensures a[\result] == val;10ensures \forall integer i; 0 <= i < \result ==> a[i] != val;1112behavior none:13assumes \forall integer i; 0 <= i < n ==> a[i] != val;14ensures \result == n;1516complete behaviors;17disjoint behaviors;18 */19 size_type find(const value_type* a, size_type n, value_type val);Listing 3.9: Formal specification of findLine 2 indicates that n is non-negative and that the pointer a points to n contiguously allocatedobjects of type value_type (see Section 1.3).Line 4 indicates that find (as a non-mutating algorithm), does not modify any memory locationoutside its scope (see Page 21).We have subdivided the specification of find into two behaviors (named some and none).The behavior some checks that the sought-after value is contained in the array.

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

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