ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (1184405), страница 10
Текст из файла (страница 10)
Since C and henceACSL, does not support an & type constructor (“declarator”), we will present an algorithm thatprocesses pointers and refer to it as swap.Our version of the original signature now reads:void swap(value_type* p, value_type* q);6.2.1. Formal Specification of swapThe ACSL specification for the swap function is shown in Listing 6.3.1 /*@2requires \valid(p);3requires \valid(q);45assigns *p;6assigns *q;78ensures *p == \old(*q);9ensures *q == \old(*p);10 */11 void swap(value_type* p, value_type* q);Listing 6.3: Formal specification of swapLines 2–3 states that both argument pointers to the swap function must be dereferenceable.Lines 5–6 formalizes that the swap algorithm modifies only the entries referenced by the pointers p and q.
nothing else may be altered. Equivalently, we could have used a clauseassigns *p, *q;instead. In general, when more than one assigns clause appears in a function’s specification,it permitted to modify any of the referenced locations. However, if no assigns clause appearsat all, the function is free to modify any memory location, see [10, Subsection 2.3.2]. Toforbid a function to do any modifications outside its scope, a clauseassigns \nothing;must be used, as we practised in the example specifications in Chapter 3.Lines 8–9 Upon termination of swap, the entries must be mutually exchanged. The expressionold(*p) refers to the pre-state of the function contract, whereas by default, a postconditionrefers the values after the functions has been terminated.3132See http://www.sgi.com/tech/stl/swap.html.See http://www.sgi.com/tech/stl/iter_swap.html.626.2.2.
Implementation of swapListing 6.4 shows the usual straight-forward implementation of swap. No interspersed ACSL isneeded to get it verified by Frama-C.123456void swap(value_type* p, value_type* q){const value_type save = *p;*p = *q;*q = save;}Listing 6.4: Implementation of swap636.3. The swap values AlgorithmThe swap values algorithm is not part of the C++ Standard Library. A call of the functionswap_values(a, n, i, j) simply swaps values a[i] and a[j] of an array a with the sizen. This could also be done using swap(a+i, a+j). Nevertheless, there are slight differencesof their formal specifications. If two values are swapped within an array, it is often important toassure that all the other elements are unchanged.
For the swap values algorithm this is ensuredby the SwapValues predicate. The stronger formal specification of swap values will be usefulfor the formal verification of the reverse algorithm, see Section 6.6 on Page 72.6.3.1. Formal Specification of swap valuesWe define a predicate SwapValues that formalizes the fact that two values a[i] and a[j] of a,and only them, are changed at a given time, here indicated by Label L2.The predicate is shown in Listing 6.5 and occurs in the formal specification which can be seen inListing 6.6.123456789/*@predicateSwapValues{L1,L2}(value_type* a, size_type i, size_type j) =0 <= i && 0 <= j &&\at(a[i],L1) == \at(a[j],L2) &&\at(a[j],L1) == \at(a[i],L2) &&(\forall integer k; 0 <= k && k != i && k != j ==>\at(a[k],L1) == \at(a[k],L2));*/Listing 6.5: The predicate SwapValuesLines 5-6 ensure that the values a[i] and a[j] are swapped.Lines 7-8 formalize that only the aforesaid values of a are swapped.
For all the rest of themnothing has changed at Label L2.64Listing 6.6 shows the specification of swap_values. Using the predicate SwapValues keeps itsimple.123456789101112/*@requires IsValidRange(a, n);requires 0 <= i < n;requires 0 <= j < n;assigns a[i];assigns a[j];ensures SwapValues{Old,Here}(a, i, j);/*void swap_values(value_type* a, size_type n,size_typei, size_type j);Listing 6.6: Formal specification of swap_values6.3.2. Implementation of swap valuesThe implementation of swap values is shown in Listing 6.7.1234567void swap_values(value_type* a, size_type n,size_typei, size_type j){value_type tmp = a[i];a[i] = a[j];a[j] = tmp;}Listing 6.7: Implementation of swap_values656.4.
The swap ranges AlgorithmThe swap ranges algorithm33 in the C++ STL exchanges the contents of two expressed rangeselement-wise. After translating C++ reference types and iterators to C, our version of the originalsignature reads:void swap_ranges(value_type* a, size_type n, value_type* b);We do not return a value since it would equal n, anyway.This function refers to the previously discussed algorithm swap. Thus, swap ranges servesas another example for “modular verification”. The specification of swap will be automaticallyintegrated into the proof of swap ranges.6.4.1.
Formal Specification of swap rangesListing 6.8 shows an ACSL specification for the swap ranges algorithm.1 /*@2requires IsValidRange(a, n);3requires IsValidRange(b, n);4//requires \separated(a+(0..n-1), b+(0..n-1));56assigns a[0..n-1];7assigns b[0..n-1];89ensures IsEqual{Here,Old}(a, n, b);10ensures IsEqual{Old,Here}(a, n, b);11 */12 void swap_ranges(value_type* a, size_type n, value_type* b);Listing 6.8: Formal specification of swap rangesLine 4 This line is commented out not only for the C compiler (by the /*@ in Line 1), but alsofor Frama-C.The swap ranges algorithm works correctly only if a and b do not overlap. For example,value_type buf[3]value_type* constvalue_type* constswap_ranges(a, 2,printf("a = { %d,printf("b = { %d,= { 10, 11, 12 };a = &buf[0];b = &buf[1];b);%d }\n",a[0],a[1]);%d }\n",b[0],b[1]);results in the outputa = { 11, 12 }b = { 12, 10 }33See http://www.sgi.com/tech/stl/swap_ranges.html.66where b is different from the old a.The separated-clause in Line 4 was intended to tell Frama-C that a and b must not overlap.
However, the separated-clause is marked “experimental” in [10, Subsection 2.7.2]and does not work for our example. Therefore, we commented it out and used a Jessiepragma to ensure the assumption that all different pointers point to disjoint locations, cf. theremarks in Section 1.4 on Page 10.Lines 6–7 The swap ranges algorithm alters the elements contained in two distinct ranges,modifying the corresponding elements and nothing else.Lines 9–10 The postconditions of swap ranges specify that the content of each element in itspost-state must equal the pre-state of its counterpart. Therefor, we can use the predicateIsEqual (see Section 3.1) together with the label Old and Here to express the postcondition of swap ranges. Line 9 of Listing 6.8, for example, specifies that the array a in thememory state that corresponds to the labels Here is equal to the array b at the label Old.Since we are specifying a postcondition Here refers to the post-state of swap rangeswhereas Old refers to the pre-state.676.4.2.
Implementation of swap rangesListing 6.9 shows an implementation of swap ranges together with the necessary loop annotations.1 void swap_ranges(value_type* a, size_type n, value_type* b)2 {3/*@4loop invariant 0 <= i <= n;56loop assigns a[0..i-1];7loop assigns b[0..i-1];89loop invariant IsEqual{Pre,Here}(a, i, b);10loop invariant IsEqual{Here,Pre}(a, i, b);11loopvariant n-i;12*/13for (size_type i = 0; i < n; i++)14swap(&a[i], &b[i]);15 }Listing 6.9: Implementation of swap rangesLines 6–7 The assigns clause declares that nothing except the sub-ranges a[0..i-1] andb[0..i-1] are modified [10, Subsection 2.4.2].
It is worth noting again the appearance ofi-1 rather than i; cf. Figure 6.10. Moreover, note that we have to allow all alterations ofall earlier loop cycles, too. For this reason, it is not sufficient to specifyloop assigns a[i-1];loop assigns b[i-1];which would be sufficient only for the current loop cycle.Lines 9–10 For the postcondition in Line 9 and 10 in Listing 6.8 to hold, loop invariants mustensure that at each iteration all of the corresponding elements that have been visited areswapped.
Note that the loop invariant has to hold after incrementing i and before the looptest i != n. Figure 6.10 shows an example run for n=2, a=[10,11], and b=[20,21].The loop invariant is checked for the memory states highlighted in green, and is valid there.Again, we can use the predicate IsEqual to express the fact that in iteration i the elementsa[0],...,a[i-1] are equal to the corresponding elements b[0],...,b[i-1] beforethe loop was entered. This expressed by binding a and b to the labels Here and Pre,respectively.This part of the loop invariant is necessary to prove the postcondition in Line 9 and 10in Listing 6.8. It is, however, not sufficient. We also need that the parts a[i..n-1] andb[i..n-1] are left unchanged by the loop body.
This additional requirement, which isoften forgotten, is entailed by the loop assigns clauses in Listing 6.9.68ni=0i!=nswapi++i!=nswapi++i!=n222222222i00011122ab0101101010202020202020111111111111212121202020101010101010212121212121111111Figure 6.10.: Loop invariant check points696.5. The copy AlgorithmThe copy algorithm in the C++ Standard Library implements a duplication algorithm for generalsequences.
For our purposes we have modified the generic implementation34 to that of a range oftype value_type. The signature now reads:void copy(const value_type* a, size_type n, value_type* b);Informally, the function copies every element from the source range a to the destination range b.The verification of copy is very similar to that of swap ranges, cf. Section 6.4.6.5.1. Formal Specification of copyThe ACSL specification of copy is shown in Listing 6.11.1 /*@2requires IsValidRange(a, n);3requires IsValidRange(b, n);4//requires \separated(a+(0..n-1), b+(0..n-1));56assigns b[0..n-1];78ensures IsEqual{Here,Here}(a, n, b);9 */10 void copy(const value_type* a, size_type n, value_type* b);Listing 6.11: Formal specification of copyLine 4 The separated-clause tells Frama-C that a and b must not overlap.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
