ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (1184405), страница 13
Текст из файла (страница 13)
Hence b[0..m-1] is a filtered copy of a[0..n-1] after removing duplicate ele-ment.6.10.3. Formal Specification of unique copyUsing the predicate UniqueCopy, we can specify the function unique_copy in an elegant way.1 /*@2requires IsValidRange(a, n);3requires IsValidRange(b, n);45assigns b[0..(n-1)];6ensures \forall integer k; \result <= k < n ==> b[k] == \old(b[k]);78ensures 0 <= \result <= n;9ensures UniqueCopy(a, n, b, \result);10 */11 size_type unique_copy(const value_type* a,12size_type n, value_type* b);Listing 6.29: Formal specification of the unique_copy functionLines 2–3 We refer to Section 1.3 for how valid ranges are specified.Lines 5–6 The algorithm modifies nothing but the destination range.Line 8 The range of the result sequence must be equal to or smaller than that of the originalsequence.Line 9 This part simply says that unique_copy should behave according to UniqueCopy.6.10.4.
Implementation of unique copyAn implementation (including loop annotations) of unique_copy is shown in Listing 6.30.Almost each loop invariant is motivated by a corresponding assertion of the specification (Listing 6.29). The former usually tells the provers how the latter is to be achieved during the loop ateach step.86123456789101112131415161718192021222324size_type unique_copy(const value_type* a, size_type n, value_type* b){if (n<=0) return 0;size_type j = 0;b[j++] = a[0];/*@loop invariant 1 <= j <= i <= n;loop assignsb[1..(j-1)];//loop invariant \forall integer k; 0 <= k <= i-1//==> WhitherUnique(a,k) <= WhitherUnique(a,i-1);loop invariant \forall integer k; 0 <= k < i==> a[k] == b[WhitherUnique(a,k)];loop invariant UniqueCopy(a, i, b, j);loopvariant n - i;/*for (size_type i = 1; i < n; i++){if (a[i] != a[i-1])b[j++] = a[i];}return j;}Listing 6.30: Implementation of the unique_copy functionLine 8 The indices i and j must stay within the range bounds.Line 9 The loop assigns clause ensures that nothing but b[0..(j-1)] is modified.
It isnecessary to prove Line 5 of the specification in Listing 6.29.Line 11–12 This loop invariant proves the monotonic feature of the logic function WhitherUnique.It is commented, because it is already included in unique_lemma_5 in the logic functionWhitherUnique in Listing 6.26. This feature will latter be used to prove Line 13–14.Line 13–14 This loop invariant is a part of UniqueCopy(a, i, b, y). It assumes that b[0..j-1]is a filtered copy of a[0..i-1].Line 15 We simply refer to the predicate UniqueCopy to specify the most essential part of theloop invariant. This is needed to prove Line 9 of the specification in Listing 6.29.Line 16 The expression n-i is always positive, and is decreased in every loop cycle, thus ensuringloop termination.876.11. The iota AlgorithmThe iota algorithm in the C++ STL assigns sequentially increasing values to a range, where thestart value is user defined.
Our version of the original signature41 reads:void iota(value_type* a, size_type n, value_type val);Starting at val, the function assigns consecutive integers to the range a. When specifying iotawe must be careful to deal with possible overflows.6.11.1. Formal Specification of iotaThe ACSL specification of iota is shown in Listing 6.31.123456789/*@requires IsValidRange(a, n);requires val + n < INT_MAX;assigns a[0..n-1];ensures \forall integer k; 0 <= k < n ==> a[k] == val + k;*/void iota(value_type* a, size_type n, value_type val);Listing 6.31: Formal specification of iotaLines 2 We refer to Section 1.3 for a discussion of how valid ranges are specified.Lines 3 is necessary to avoid integer overflows in iota.Line 5 The iota algorithm initializes and modifies the elements in range a. Elements outsidethe range a[0..n-1] are not altered.Line 7 Upon termination, each element of a contains the sum of its index within a and the argument val.41See http://www.sgi.com/tech/stl/iota.html.886.11.2.
Implementation of iotaListing 6.32 shows an implementation of the iota function.12345678910111213void iota(value_type* a, size_type n, value_type val){/*@loop invariant 0 <= i <= n;loop assigns a[0..i-1];loop invariant \forall integer k; 0 <= k < i ==> a[k] == val + k;loopvariant n-i;*/for (size_type i = 0; i < n; i++)a[i] = val + i;}Listing 6.32: Implementation of iotaLine 4 indicates that the loop index must stay within bounds.Line 6 The assigns clause ensures that nothing but the range a is modified.Line 8 This loop invariant ensures that for each iteration, the elements contain the proper value.It is essential to prove the postcondition in Line 7 in Listing 6.31.Line 9 provides a positive expression which is decreased in every loop iteration to prove looptermination.897.
Heap OperationsWe cite the Apache C++ Standard Library User’s Guide heap operations:A heap is a binary tree in which every node is larger than the values associated witheither child. A heap and a binary tree, for that matter, can be very efficiently stored ina vector, by placing the children of node i at positions 2i + 1 and 2i + 2.Using this encoding, the largest value in the heap is always located in the initial position, and can therefore be very efficiently retrieved. In addition, efficient logarithmicalgorithms exist that permit a new element to be added to a heap and the largest element removed from a heap.
For these reasons, a heap is a natural representation forthe priority queue data type.42Figure 7.1 shows the binary tree of the heap indices 0, 1, . . . , (n-1) for n = 12.01237489510611Figure 7.1.: Binary tree of the heap indices 0, 1, . . . , 11Only in case the heap-size n is even, there is exactly one parent node with one child only. All othernodes have two or no children at all.As mentioned in the citation above for performance reasons a (complete) ordering of the heap’sdata array is not appropriate . The fractional ordering—parents value is not less than children’svalues— is called weak ordering. This weak ordering can be maintained with logarithmic effort.In this chapter we consider various heap-related algorithms:is heap from Section 7.2 allows to test at run time whether a given array is arranged as a heap.push heap from Section 7.3 adds an element to a given heap in such a way that resulting arrayis again a heap.42See Section 14.7 in http://stdcxx.apache.org/doc/stdlibug/14.html91pop heap from Section 7.4 removes an element from a given heap in such a way that the resulting array is again a heap.make heap from Section 7.5 turns a given array into a heap.sort heap from Section 7.6 turn a given heap into a sorted range.heap sort from Section 7.7 does not directly correspond to an STL algorithms.
It usesmake heap and sort heap to implement a robust sorting algorithm.The essential predicates that formalize the properties of heap are introduced in Section 7.1.In this chapter, we deliberately omitted all properties speaking about preservation of array contents.For example, the function contract of heap_sort ensures the the resulting array is ordered, but itdoes not ensure that it contains the same elements as before the heap_sort-call. Such a specification could also be implemented by assigning 0 to all heap elements c[i], which is certainlynot what a user of this algorithm has in mind.
It is a common pitfall to forget to specify contentspreservation properties, since they seem to be all too obvious to be kept in mind explicitly.We will supply the missing specification parts and the corresponding correctness proofs in a coming issue of this tutorial. Here we only indicate this gap by placing a non-ACSL comment// ensures Permutation\{Old, Here\}(c, n)}in each of the function contracts.927.1.
Axiomatic Description of HeapsThe ACSL specification for the edge relation ParentChild in the tree and the definition of theheap’s weak ordering predicate IsHeap is shown in Listing 7.2.The meanings of axiom ParentChild_1 and axiom ParentChild_2 are identical, however(up to now) the provers “don’t know it” or cannot proof it. It depends on the upwards or downwardsdirection the tree algorithms are operating which of these axioms is to be applied.The lemma ParentChild_3 can be proved and is a necessary hint for the provers in the verification processes.12345678910111213141516171819202122/*@axiomatic ParentChildAxioms{predicate ParentChild(integer i, integer j);axiom ParentChild_1:\forall integer i, j; ParentChild(i, j) <==>0 <= i < j && (j == 2*i+1 || j == 2*i+2);axiom ParentChild_2:\forall integer i, j; ParentChild(i, j) <==>0 < j && i == (j-1)/2;}lemma ParentChild_3:\forall integer i; 0 < i ==>ParentChild((i-1)/2, i) && 0 <= (i-1)/2 < i;predicate IsHeap{L}(value_type* c, integer n) =\forall integer i, j;j < n && ParentChild(i, j) ==> c[i] >= c[j];*/Listing 7.2: The ParentChild and IsHeap predicatesParentChild(i,j) holds if the heap index i corresponds to the parent node of the node corresponding to index j.
Note that it does not depend on the contents of the heap array.IsHeap(c,n) holds if the array c[0..n-1] forms a heap in the sense of the above definitionfrom the STL User’s Guide (Page 91), i.e. if it is weakly ordered.937.2. The is heap AlgorithmThe function is heap tests whether a given array has the heap-property described on Page 7.The is heap algorithm of the STL in the Library works on generic sequences. For our purposeswe have modified the generic implementation43 to that of an array of type value_type. Thesignature now reads:bool is_heap(const value_type* a, int n);7.2.1. Formal Specification of is heapThe ACSL specification of is heap is shown in Listing 7.3.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
