ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (1184405), страница 14
Текст из файла (страница 14)
The function returns true if andonly if its argument satisfies the properties of a heap.12345678/*@requires IsValidRange(c, n);assigns \nothing;ensures \result <==> IsHeap(c, n);*/bool is_heap(const value_type* c, size_type n);Listing 7.3: Function contract of is heap43See http://www.sgi.com/tech/stl/is_heap.html. Note that is heap is not part of the C++ standardlibrary.947.2.2.
Axiomatic Description of Even and Odd NumbersOur implementation of IsHeap uses the distinction of even and odd numbers to increase run-timeefficiency. It test whether a number is even or odd by using the C operator & for bit-wise and. As itturns out we need additional axioms (see Listing 7.4 to help the provers understanding propertiesof operator &.12345678910111213141516171819/*@axiomatic Ampersand{predicate Even(integer i) = (i&1) == 0;predicate Odd(integer i)= (i&1) == 1;axiom Ampersand_1: \forall integer i;Odd(i) && Even(i+1) || Even(i) && Odd(i+1);axiom Ampersand_2: \forall integer i;i > 0 && Odd(i) ==> (i-1)/2 == i/2;axiom Ampersand_3: \forall integer i;i > 0 && Even(i) ==> (i-1)/2 + 1 == i/2;}lemma Ampersand_0: Even(0); // not needed as axiom*/Listing 7.4: The predicates Even and Odd.We suppose that our readers are familiar with the properties stated by the axioms.
We thereforegive only short explanation of the axioms in Listing 7.4.Axiom Ampersand 1 states that integers in their natural order are alternating even or odd.Axiom Ampersand 2 says with other words in our heap-tree terminology: If i > 0 and i isodd, then child i and child i+1 have the same parent.Axiom Ampersand 3 is similar to Ampersand 2.Lemma Ampersand 0 shows that the prover “knows” something about the function x -> x&1.It is interesting, that neither in the specification nor in the implementation of is_heap the predicates Even and Odd are explicitly used.957.2.3. Implementation of is heapListing 7.5 shows one way to implement the function is heap.1 bool is_heap(const value_type* c, size_type n)2 {3size_type parent = 0;4/*@5loop invariant 0 <= parent < child <= n+1;67loop invariant parent == (child-1)/2;8loop invariant \forall integer i;90 < i < child ==> c[(i-1)/2] >= c[i];1011loop invariant IsHeap(c, child-1);12loopvariant n - child;13*/14for (size_type child = 1; child < n; child++)15{16if (c[parent] < c[child])17return false;1819if ((child & 1) == 0)20{21//@ assert ParentChild(parent+1, child+1);22parent++;23}24//@ assert (child & 1) == 1 ==> ParentChild(parent, child+1);25}26return true;27 }Listing 7.5: Implementation of is heapThe working scheme of is heap is easily to explain with Figure 7.6.012345678910 11Figure 7.6.: Array sight of the binary heap treeWhile incrementing a child it may happen, that the corresponding parent does not change or alternatively that the parent must also be incremented.
The second variant happens exactly in case thechild is even. The implementation of is heap exploits this to traverse the complete binary heaptree.96Lines 19–23 in connection with the parent initialization and the for-loop are responsible for thetree parsing.Line 7 This loop invariant preserves the parent-child connection.Lines 8–11 establish the heap property as long the test if (c[parent] < c[child]) failed.Lines 21 and 24 are hints given to the prover.Finally we remark that the slightly different program of Listing 7.7 would be much easier to verify.12345678bool simple_is_heap(const value_type* c, size_type n){for (size_type i = 1; i < n; i++)if (c[i] > c[(i-1)/2])return false;return true;}Listing 7.7: An implementation of is heap that is easier to verifyHowever, the former one is more interesting for two reasons.1.
Memory access is costly and an optimizing compiler can more easily avoid the memoryaccess to parent’s value in every second iteration step.2. It was a challenge to find and exploit the even/odd axioms of Listing 7.4. There is forexample the interesting fact, that after substituting axiom D1 for Even(i) ==> Odd(i+1)and Odd(i) ==> Even(i+1) the prover seems to enter an endless loop.977.3. The push heap AlgorithmThe push heap algorithm adds an element that is at the end of an array to an existing heapconsisting of the prior elements in the array. When push heap returns, the heap-property of thewhole array including the new element is established. Whereas in the STL push heap works ona pair of random access iterators,44 our version operators on a range of value_type.
Thus thesignature of push heap readsvoid push_heap(value_type* c, size_type n);7.3.1. Formal Specification of push heapListing 7.8 shows our formal specification of push heap in ACSL.1 /*@2requires n > 0;3requires IsValidRange(c, n);4requires IsHeap(c, n-1);56assigns c[0..(n-1)];78ensures IsHeap(c, n);9// ensures Permutation{Old, Here}(c, n);10 */11 void push_heap(value_type* c, size_type n);Listing 7.8: Specification of push heapLine 2 n > 0 is required because at least the “new” element c[n-1] must be in the array.Line 4 requires that before the call of push_heap all the prior elements form a heap.Line 8 ensures that after the call all the elements including c[n-1] form a heap.Line 9 indicates the missing content-preservation specification.44See http://www.sgi.com/tech/stl/push_heap.html987.3.2.
Implementation of push heapListing 7.9 shows the implementation of push heap.12345678910111213141516171819202122232425262728void push_heap(value_type* c, size_type n){const value_type tmp = c[n-1];size_type hole = n-1;/*@loop invariant 0 <= hole < n;loop invariant hole < n-1 ==> IsHeap(c, n);loop invariant \forall integer i, j;j < n && j != hole && ParentChild(i, j) ==> c[i] >= c[j];loop invariant \forall integer i;i < n && ParentChild(hole, i) ==> c[i] <= tmp;loopvariant hole;*/while (hole > 0){const size_type parent = (hole-1)/2;if (c[parent] < tmp)c[hole] = c[parent];elsebreak;hole = parent;}c[hole] = tmp;}Listing 7.9: Implementation of push heapLine 3 saves the new element c[n-1] in a variable tmp andLine 4 initializes hole with the top index n-1.Lines 16–26 The loop is searching for the right place for the new element tmp by moving thehole upwards and shifting down the passed elements.
In each loop step the position holeis tested whether it is the right place to store tmp.Line 27 The right place hole for tmp has been found now and tmp can be dropped.Lines 8–10 These loop invariants are needed to guarantee finally the heap property. Note thatIsHeap(c, n) is valid only after the first iteration step.Lines 12–13 This invariant ensures that dropping tmp to the final hole-place does not destroythe heap property.99Figure 7.10 illustrates the iteration steps of the push_heap function. When push_heap(c, 12)is called, the range c[0..10] forms a valid heap, and c[11] contains the value 77 that has beenrecently appended. The task of push_heap is to move the new 77 to its appropriate place in orderto make the whole range c[0..11] a valid heap.First, the 77 is moved from c[11] to the local variable tmp (Line 3 in Listing 7.9).
Thereby, weget a “hole” at c[11] (Line 4). The loop in Lines 16–26 will move that hole upwards in the treeuntil the 77 can be dropped (Line 27) without violating the heap property.In the first loop cycle, we compare the 8 at the parent position c[5] against the 77. Since the 77is still larger, we move the hole one level upwards in the tree, i.e. we move the 8 downwards. Theresulting situation is depicted in Figure 7.10.In the second cycle, we similarly compare the 17 at c[2] against the 77, and move the hole up toc[2].
In the third cycle, we move the hole up again, to c[0]. After that, we leave the loop sincehole > 0 in Line 16 no longer holds, and drop the 77 to c[0]. Now the whole range c[0..11]is a valid heap.110422421717nexthole59118hole8107038117777tmpFigure 7.10.: An iteration step of push_heap100137.4. The pop heap AlgorithmThe function pop heap is in some sense converse to push heap (see Section 7.3). It moves thelargest element from the front of a heap to the last position in the array and then forms a new heapfrom the remaining elements.Whereas in the STL pop heap works on a pair of random access iterators,45 our version operatorson a range of value_type.
Thus the signature of pop heap readsvoid pop_heap(value_type* c, size_type n);7.4.1. Formal Specification of pop heapThe function contract of pop heap in ACSL is given by Listing 7.11.Note in Line 10 the use of the predicate IsMaximum from Listing 4.5.12345678910111213/*@requires 0 < n < (INT_MAX-2)/2;requires IsValidRange(c, n);requires IsHeap(c, n);// assigns c[0..(n-1)];ensures IsHeap(c, n-1);ensures c[n-1] == \old(c[0]);ensures IsMaximum(c, n, n-1);// ensures Permutation{Old, Here}(c, n);*/void pop_heap(value_type* c, size_type n);Listing 7.11: Function contract of pop heapLine 6 The property that only the elements of c are assigned is commented out here.
It seems thatadding this little bit overburdens the provers. However we were able to prove it separatelyby omitting other proof goals (Line 4, 8–10 in the specification in Listing 7.11, Line 3–4,16–20, 47–49 in the implementation in Listing 7.14).Line 8 ensures that the remaining elements form a heap of length n - 1.Lines 9–10 ensure that the maximal element of the input heap is finally at the last position n - 1.Here we use the IsMaximum predicate from Listing 4.5 in Section 4.2.Line 11 indicates the missing content-preservation specification.45See http://www.sgi.com/tech/stl/pop_heap.html1017.4.2.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
