ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (1184405), страница 12
Текст из файла (страница 12)
The remove copy AlgorithmThe remove copy algorithm of the C++ Standard Library allows to remove specific elementsfrom general sequences. Here, the general implementation has been altered to process value_typeranges.39 The new signature reads:size_type remove_copy(const value_type* a, size_type n,value_type* b, value_type v);The most important facts of this algorithms are1. The remove copy algorithm copies elements that are not equal to v in the range a[0, n-1]to a range beginning at b[0].2.
The return value is the length of the resulting range.3. This operation is stable, meaning that the relative order of the elements in b is the same asin a.Again, we need to issue appropriate command-line options to tell Frama-C that the ranges a andb must not overlap.6.9.1.
A Predicate for remove copyEven though it is possible to define a predicate RemoveCopy in one axiomatic scheme we will doit in two steps for simplicity reason. First we define a logic integer function WhitherRemovepointing in particular for each index i with a[i] != v to the position in array b whereto theelement a[i] has to be copied.
For all other indices WhitherRemove is pointing to “the nextfree place”. An example is shown in Figure 6.21.vabvvavcdve012345678910012345678910Figure 6.21.: Exemplified application of the logic function WhitherRemove39See http://www.sgi.com/tech/stl/remove_copy.html.80The ACSL axiomatic of WhitherRemove is given in Listing 6.22.12345678910111213141516171819202122/*@axiomatic WhitherRemove_Function{logic integer WhitherRemove{L}(value_type* a, value_type v,integer i) reads a[0..(i-1)];axiom whither_1:\forall value_type *a, v; WhitherRemove(a , v, 0) == 0;axiom whither_2:\forall value_type *a, v, integer i; a[i] == v ==>WhitherRemove(a, v, i+1) == WhitherRemove(a, v, i);axiom whither_3:\forall value_type *a,v, integer i; a[i] != v ==>WhitherRemove(a, v, i+1) == WhitherRemove(a, v, i) + 1;axiom whither_lemma:\forall value_type *a, v, integer i, j; i < j && a[i] != vWhitherRemove(a, v, i) < WhitherRemove(a, v, j);==>}*/Listing 6.22: Axiomatic of the logic function WhitherRemoveLines 4–5 define the signature of the function WhitherRemove.
Additionally, a reads clauseis used to state that the value of WhitherRemove depends only on the contents ofa[0..(i-1)]. Although this property is a consequence of the definition in Lines 7–12, weneed to state it explicitly, since none of the provers is able to establish it by itself.Axiom whither 1 state that at beginning the first free place is 0.Axiom whither 2 state that for a[i] != v the next free place is incremented by one becausethe element a[i] has to be copied.Axiom whither 3 state that for a[i] == v the next free place is unchanged.Axiom whither lemma is actually a consequence of the other axioms.
However as lemma it canbe proven by induction only and this is impossiple with ACSL. Because later on it will beneeded we have added it as axiom.81It is easy now to define the RemoveCopy predicate needed in the specification of remove copy.12345678/*@predicateRemoveCopy{L}(value_type* a, integer n,value_type* b, integer m, value_type v) =m == WhitherRemove(a, v, n) &&\forall integer i;0 <= i < n && a[i] != v ==> b[WhitherRemove(a, v, i)] == a[i];*/Listing 6.23: The predicate RemoveCopyHere we only have keep in mind that all elements a[i] != v are to be copied tob[WhitherRemove(a,v,i)] and that finally the first free position equals m.6.9.2. Formal Specification of remove copyUsing the predicate RemoveCopy, we can specify the function contract of remove copy in abrief and elegant way, as shown in Listing 6.24.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 RemoveCopy(a, n, b, \result, val);9 */10 size_type remove_copy(const value_type* a, size_type n,11value_type* b, value_type val);Listing 6.24: Formal specification of the remove copy functionLines 5–6 The algorithm modifies nothing but the destination range.To specify this, the most convenient way would be:assigns b[0..\result-1];However, the assigns clause refers to the pre-state of the function, where the identifier\result is unknown.
We therefore added Line 6 to express that the range b[\result..n)is not changed.Line 8 This is the essential part of the specification. It simply says that remove copy shouldbehave according to RemoveCopy.826.9.3. Implementation of remove copyAn implementation (including loop annotations) of remove copy is shown in Listing 6.25.1234567891011121314151617size_type remove_copy(const value_type* a, size_type n,value_type* b, value_type v){size_type j = 0;/*@loop assigns b[0..(j-1)];loop invariant 0 <= j <= i <= n;loop invariant RemoveCopy(a, i, b, j, v);loop variant n - i;*/for (size_type i = 0; i < n; i++){if (a[i] != v)b[j++] = a[i];}return j;}Listing 6.25: Implementation of the remove copy functionAlmost each assertion of the loop invariant is motivated by a corresponding assertion of the specification (Listing 6.24). The former usually tells the provers how the latter is to be achieved duringthe loop at each step.Line 6 The loop assigns clause ensures that nothing but b[0..j-1] is modified.
It is neces-sary to prove Line 7 of the specification.Line 7 The indices i and j must stay within the range bounds. Moreover, we always havej <= i; the latter is needed to prove that j <= n holds .Line 8 Again, we simply refer to the predicate RemoveCopy to specify the most essential partof the loop invariant. This is needed to prove Line 8 of the specification in Listing 6.24.Line 9 The expression n-i is always positive, and is decreased in every loop cycle, thus ensuringloop termination.836.10. The unique copy AlgorithmThe unique copy algorithm of the C++ Standard Library allows to remove duplicate elementsfrom general sequences. Here, the general implementation40 has been altered to process value_typeranges. The new signature reads:size_type unique_copy(const value_type* a,size_type n, value_type* b);The unique copy algorithm copies elements in the range a[0..n-1] to a range beginning atb[0], but of a consecutive group of duplicate elements only the first one is copied.
The returnvalue is the length of the resulting range.6.10.1. The Logic Function WhitherUniqueThe ACSL specification of unique_copy refers to the logic function WhitherUnique definedby axioms shown in Listing 6.26.1 /*@2axiomatic WhitherUnique_Function3{4logic integer WhitherUnique{L}(value_type* a, integer i)5reads a[0..i];67axiom unique_1: \forall value_type *a;8WhitherUnique(a,0) == 0;910axiom unique_2: \forall value_type *a, integer i;11a[i] == a[i+1] ==> WhitherUnique(a,i+1) == WhitherUnique(a,i);1213axiom unique_3: \forall value_type *a,v, integer i;14a[i] != a[i+1] ==>15WhitherUnique(a,i+1) == WhitherUnique(a,i) + 1;1617axiom unique_lemma_4: \forall value_type *a, integer i,j;18i < j && a[i] != a[i+1] ==>19WhitherUnique(a,i) < WhitherUnique(a,j);2021axiom unique_5: \forall value_type *a, integer i,j;22i < j ==> WhitherUnique(a,i) <= WhitherUnique(a,j);23}24 */Listing 6.26: The Logic Function WhitherUniqueThe predicate WhitherUnique(a, i) helps to locate the positions of the elements in the resultsequence.
If an element is in position i in the source sequence, then it will appear in positionWhitherUnique(a,i) in the result sequence, which means a[i]=b[WhitherUnique(a,i)].40See http://www.sgi.com/tech/stl/unique_copy.html.84Therefore b[0..WhitherUnique(a,i)] is a filtered copy of a[0..i], in a consecutive groupof duplicate elements only the first one is copied. An example is shown in figure 6.27, solid arrowindicating an actual copy, and dashed arrows indicating a redundant, and hence omitted, copy.aabbbccdcce012345678910012345678910Figure 6.27.: An Example of the Logic Function WhitherUniqueWe give some explanations about the axiomatic definition from Listing 6.26.Lines 4–5 Here we defined the signature of the predicate WhitherUnique.Axiom unique 1 states the situation for the first element of a.
It is simply copied to the beginningof the result sequence.Axiom unique 2 assumes that the result sequence for a[0..i] has WhitherUnique(a,i)elements and that a[i] equals a[i+1], i.e., the latter should be removed. It states that underthese circumstances, the result sequence for a[0..i+1] has also WhitherUnique(a,i)elements.Axiom unique 3 assumes again that the result sequence for a[0..i] has WhitherUnique(a,i)elements, but a[i] is now different from a[i+1]. It states that if in this situation a[i+1]is copied to the result sequence, then the result sequence for a[i+1] hasWhitherUnique(a,i)+1 elements.Axiom unique lemma 4 and 5 assume the monotonicity of the logic function WhitherUnique,which will be used in the proof of the loop invariant in Line 13–14 in Listing 6.30.
Although they both are consequences of axioms unique_1..3, we didn’t prove, but simplyrequired them here. These lemmas tell the provers how the latter is to be achieved, whichmeans without the lemmas the provers will not know, how to prove unique copy.6.10.2. Predicate UniqueCopy for unique copyThe ACSL specification of unique_copy refers to a predicate UniqueCopy shown in Listing 6.28.The predicate UniqueCopy(a,n,b,m) formalizes two facts. One is that when the sequence a hasat least one element, then m-1 = WhitherUnique[a,n-1], which means the result sequencefor a[0..n-1] has m-1 elements. Another is that a[i] = b[WhitherUnique(a,i)] for all8512345678/*@predicateUniqueCopy{L}(value_type* a, integer n,value_type* b, integer m) =(n == 0 ==> m == 0) &&(n >= 1 ==> m-1 == WhitherUnique(a,n-1)) &&\forall integer i; 0 <= i < n ==> a[i] == b[WhitherUnique(a,i)];*/Listing 6.28: The Predicate UniqueCopy0 <= i < n.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
