ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (1184405), страница 15
Текст из файла (страница 15)
Handling Induction in pop heapBefore we show the implementation of pop heap we want to discuss a problem that we encountered during verification.It is obvious that, due to the heap property of the original array, the maximal element is at position0. However, if we take a closer look at the formalization of this fact, we see that the predicateIsHeap(c,n) in Listing 7.2 establishes facts likec[0]c[0]c[1]c[1]c[2]c[2]<=<=<=<=<=<=c[1]c[2]c[3]c[4]c[5]c[6]hencehencehencehencec[0]c[0]c[0]c[0]<=<=<=<=c[3]c[4]c[5]c[6]...While it is immediately obvious to a human that all these facts together imply the minimality ofc[0], an automated theorem prover is unable to• derive all these facts,• derive transitivity consequences from arbitrary-length (<=)-chains,• observe their regular structure, i.e.
that c[0] <= c[i] can eventually be derived for eachi < n, and• conclude that \forall integer i; i < n ==> c[0] <= c[i] holds.All the more, it cannot do this in a single step, like humans can do. Rather, it needs to perform aproof by induction on n to establish the desired conclusion\forall integer i; i < n ==> c[0] <= c[i].Although none of the provers employed by Frama-C is prepared to do induction proofs, we founda way to make them doing it, abusing Hoare’s loop rule (cf.
Sections 2.5 and 2.6) for that purpose.We define a C function pop_heap_induction that does not contribute to the functionality ofpop_heap, but rather encapsulates the induction proof needed for its verification. This function will be called as ghost. The function contract of pop_heap_induction, shown in Listing 7.12, essentially requires our assumption, viz. IsHeap(c,n) and ensures our proof goal,viz. \forall integer i; 0 <= i < n ==> c[0] >= c[i].In order to cause the prover to do an induction on n, we use a for-loop (Lines 3–12 in Listing 7.13)with a corresponding range and the induction hypothesis as loop invariants. The loop bodyis empty, except for an additional hint to the prover in Line 11.One can see in Listing 7.13 that a loop with an empty body makes perfectly sense.
The assertionin Line 11 of Listing 7.13 is necessary to help the automatic provers.102123456789/*@requires 0 < n && IsValidRange(c, n);requires IsHeap(c, n);assigns \nothing;ensures \forall integer i; 0 <= i < n ==> c[0] >= c[i];/*void pop_heap_induction(const value_type* c, size_type n);Listing 7.12: Contract of ghost-function to perform induction12345678910111213void pop_heap_induction(const value_type* c, size_type n){/*@loop invariant 0 <= i <= n;loop invariant \forall integer j;0 <= j < i <= n ==> c[0] >= c[j];loopvariant n - i;*/for (size_type i = 1; i < n; i++){//@ assert 0 < i ==> ParentChild((i-1)/2, i);}}Listing 7.13: Implementation of the ghost-function to perform induction1037.4.3.
Implementation of pop heapThe implementation of pop heap is shown in Listing 7.14 and is considerably more complexthan that of push heap (see Listing 7.9).In push heap we were traversing the binary heap tree bottom-up. Thereby every node hadat most one parent, there was no choice. Now, in the case of pop heap the tree traversingoperates downwards and in every loop step the appropriate child must be chosen. Additionally, weinclude like the corresponding algorithm of the C++ standard library an optimization concerningthe number of comparisons which must be done in each loop step.Lines 3–4 perform the induction described in Section 7.4.2.Line 6 saves the maximum to put it finally to the position n-1.Lines 16–17 support the proof that the max is the largest one at end.Lines 18–19 and the assertion in Lines 47–48 support the proof that the final dropping of tmp tothe hole-position does not destroy the heap property.Lines 22–46 The loop tests in each step, whether hole is the right position for tmp.
If not, itpercolates down the position hole to the appropriate child-position and shifts upward thecorresponding child element.Line 25 We test only, whether the larger child-position is smaller than n-1. If the answer is truethe corresponding test for the smaller child is dispensable. This way we have in one loopstep three comparisons only and not four. The case that a parent has exactly one child (thesmaller one) can occur only at the loop end and is dealt with in Lines 37–45Line 34 The break is performed if hole is the right position for the value stored in tmp.Line 39 asks among others whether the smaller child is the only one.
In this case it depends onits value whether a further step must be done.Line 44 The break exits the loop because here the right position for tmp must be found.Line 50 puts tmp that equals the former element c[n-1] to its final place hole.Line 51 puts max to the position n - 1.10412345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152void pop_heap(value_type* c, size_type n){//@ ghost pop_heap_induction(c, n);//@ assert \forall integer i; 0 < i < n ==> c[0] >= c[i];value_type tmp = c[n-1];value_type max = c[0];size_type hole = 0;/*@loop invariant 0 <= hole < n;loop assigns c[0..hole];loop invariant IsHeap(c, n-1);loop invariant \forall integer i;0 <= i < n ==> c[i] <= max;loop invariant \forall integer i;hole < n-1 && ParentChild(i, hole) ==> c[i] >= tmp;loopvariant n - hole;*/while (1){size_type child = 2*hole + 2;if (child < n-1){if (c[child] < c[child-1]) child--;//@ assert ParentChild(hole, child);if (c[child] > tmp){c[hole] = c[child];hole = child;}else break;}else{child = 2*hole + 1;if (child == n-2 && c[child] > tmp){c[hole] = c[child];hole = child;}break;}}/*@ assert \forall integer i;hole < n-1 && ParentChild(i, hole) ==> c[i] >= tmp;*/c[hole] = tmp;c[n-1] = max;}Listing 7.14: Implementation of pop heap105Figure 7.15 illustrates an iteration step of the pop_heap function.
The dashed arrows show whathas been done before.77max77424242hole13171110nexthole17709813333tmpFigure 7.15.: An iteration step of pop_heap7.5. The make heap AlgorithmWhereas in the STL make heap works on a pair of generic random access iterators,46 our versionoperators on a range of value_type. Thus the signature of make heap readsvoid make_heap(value_type* c, size_type n);The function make_heap rearranges the elements of the given array c[0..n-1] such that theyform a heap.7.5.1.
Formal Specification of make heapThe ACSL specification of make heap is shown in Listing 7.16. Line 2 prevents numeric overflow. Line 8 indicates the missing content-preservation specification.7.5.2. Implementation of make heapThe implementation of make heap, shown in Listing 7.17, is straightforward. From low to highthe array’s elements were pushed to the growing heap. The iteration starts with two, because anarray with length one is a heap already.46See http://www.sgi.com/tech/stl/make_heap.html10612345678910/*@requires n < INT_MAX;requires IsValidRange(c, n);assigns c[0..(n-1)];ensures IsHeap(c, n);// ensures Permutation{Old, Here}(c, n);*/void make_heap(value_type* c, size_type n);Listing 7.16: The specification of make_heap1234567891011void make_heap(value_type* c, size_type n){if (n == 0) return;/*@loop invariant IsHeap(c, i-1);loop invariant 2 <= i <= n+1;loopvariant n - i;*/for (size_type i = 2; i <= n; i++)push_heap(c, i);}Listing 7.17: The implementation of make_heap1077.6.
The sort heap AlgorithmThe function sort heap takes an array c[0..n-1] with the heap-property as input and sorts itselements in ascending order. Thus the signature of sort heap readsvoid sort_heap(value_type* c, size_type n);Note that in the STL sort heap works on a pair of generic random access iterators,477.6.1. Formal Specification of sort heapThe ACSL specification of sort heap is given in Listing 7.18. Line 2 prevents amongst othersnumeric overflow. Line 8 indicates the missing content-preservation specification.1 /*@2requires 0 < n < (INT_MAX-2)/2 && IsValidRange(c, n);3requires IsHeap(c, n);45assigns c[0..n-1];67ensures \forall integer i; 0 <= i < n-1 ==> c[i] <= c[i+1];8// ensures Permutation{Old, Here}(c, n);9 */10 void sort_heap(value_type* c, size_type n);Listing 7.18: The specification of sort_heap7.6.2.
Implementation of sort heapThe implementation of sort heap is shown in Listing 7.19.The iteration of sort_heap operates from high to low with respect to the numbers pop_heap iscalled with.Line 5 states that the elements below i form a heap andLines 7–8 state that the other elements including the ith are already sorted.Line 6 is the most interesting one.
In the next iteration step the element c[0] will be put in frontof c[i]. Therefore it is not allowed to be larger than c[i].47See http://www.sgi.com/tech/stl/sort_heap.html10812345678910111213void sort_heap(value_type* c, size_type n){/*@loop invariant 0 <= i <= n;loop invariant IsHeap(c, i);loop invariant i < n ==> c[0] <= c[i];loop invariant \forall integer j;i <= j < n-1 ==> c[j] <= c[j+1];loopvariant i;/*for (size_type i = n; i > 0; i--)pop_heap(c, i);}Listing 7.19: The implementation of sort_heap1097.7.
The Sorting Algorithm heap sortClearly, the concatenation of make heap (Section 7.5) and sort heap (Section 7.6) is a sortingalgorithm that is commonly referred to as heapsort.48Listing 7.20 shows the ACSL specification of heap sort. Note that the postcondition in thecomment in Line 7 is the only missing piece to achieve a complete specification of a sortingalgorithm.123456789/*@requires 0 < n < (INT_MAX-2)/2 < INT_MAX && IsValidRange(c, n);assigns c[0..(n-1)];ensures \forall integer i; 0 <= i < n-1 ==> c[i] <= c[i+1];// ensures Permutation{Old, Here}(c, n);*/void heap_sort(value_type* c, size_type n);Listing 7.20: The specification of heap_sortThe implementation of heap sort is shown in Listing 7.21.12345void heap_sort(value_type* c, size_type n){make_heap(c, n);sort_heap(c, n);}Listing 7.21: The implementation of heap_sort48See http://en.wikipedia.org/wiki/Heapsort1108.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
