ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (1184405), страница 4
Текст из файла (страница 4)
We verified that i remains a valid index into a[] provided it was valid before. Note the useof the implication rule to establish preconditions for the assignment rule as needed, and to unifythe postconditions of the then and else branch, as required by the choice rule.16//@ P && BQ//@ S//@ P && ! BR//@ Sand{//@ Pif (B) {Q} else {R}//@ SFigure 2.9.: The choice rule//@ 0 <= i <if (i < n //@ 0 <= i//@ 1 <= ii = i+1;//@ 1 <= i//@ 0 <= i} else {//@ 0 <= i//@ 0 == 0i = 0;//@ i == 0//@ 0 <= i}//@ 0 <= i <n1) {< n - 1+ 1 < ngiven precondition< n< nby the assignment ruleweakened by the implication rule== n - 1 < n&& 0 < nusing that then condition i<n-1 fails in the else partweakened by the implication rule&& 0 < n< nby the assignment ruleweakened by the implication rulenby the choice rule from the then and the else partusing that the condition i<n-1 holds in the then partby the implication ruleFigure 2.10.: An example application of the choice rule2.5.
The Loop RuleThe loop rule, shown in Figure 2.11, is used to verify a while loop. This requires to find anappropriate formula, P, which is preserved by each execution of the loop body. P is also called aloop invariant.//@ P && BS//@ P{//@ Pwhile (B) {S}//@ ! B && PFigure 2.11.: The loop rule17To find it requires some intuition in many cases; for this reason, automatic theorem provers usuallyhave problems with this task.As said above, the loop rule does not guarantee that the loop will always eventually terminate.
Itmerely assures us that, if the loop has terminated, the postcondition holds. To emphasize this, theproperties verifiable with the Hoare Calculus are usually called “partial correctness” properties,while properties that include program termination are called “total correctness” properties.As an example application, let us consider an abstract ring-buffer loop as shown in Figure 2.12.//@ 0 < n//@ 0 <= 0 < nint i = 0;//@ 0 <= i < nwhile (!done) {//@ 0 <= i < n && !donea[i] = getchar();//@ 0 <= i < n && !done//@ 0 <= i < nif (i < n-1) i++; else i = 0;//@ 0 <= i < nprocess(a,i,&done);//@ 0 <= i < n}//@ 0 <= i < ngiven preconditionfollows triviallyby the assignment rulemay be assumed by the loop rulerequired property of getcharweakened by the implication ruleas seen above (Figure 2.10)required property of processby the loop ruleFigure 2.12.: An abstract ring buffer loopFigure 2.12 shows a verification proof for the index i lying always within the valid range [0..n-1]during, and after, the loop.
It uses the proof from Figure 2.10 as a sub-part. Note the followingissues:• To reuse the proof from Figure 2.10, we had to drop the conjunct !done, since we didn’tconsider it in Figure 2.10. In general, we may not infer//@ P && SQ//@ R && Sfrom//@ PQ//@ Rsince the code fragment Q may just destroy the property S. This is obvious for Q being thefragment from Figure 2.10, and S being e.g. n != 0.Suppose for a moment that process had been implemented in way such that it refuses to setdone to true unless it is false at entry. In this case, we would really need that !done stillholds after execution of Figure 2.10. We would have to do the proof again, looping-throughan additional conjunct !done.• We have similar problems to carry the property 0 <= i < n && !done and 0 <= i < nover the statement a[i]=getchar() and process(a,i,&done), respectively. We need18to specify that neither getchar nor process is allowed to alter the value of i or n.
InACSL, there is a particular language construct assigns for that purpose, which is introduced in Section 6.2 on Page 62.• In our example, the loop invariant can be established between any two statements of theloop body. However, this need not be the case in general. The loop rule only requires theinvariant holds before the loop and at the end of the loop body. For example, processcould well change the value of i7 and even n intermediately, as long as it re-establishes theproperty 0 <= i < n immediately prior to returning.• The loop invariant, 0 <= i < n, is established by the proof in Figure 2.10 also after termination of the loop. Thus, e.g., a final a[i]=’\0’ after the loop would be guaranteed notto lead to a bounds violation.• Even if we would need the property 0 <= i < n to hold only immediately before theassignment a[i]=getchar(), since, e.g., process’s body didn’t use a or i, we wouldstill have to establish 0 <= i < n as a loop invariant by the loop rule, since there is noother way to obtain any property inside a loop body.
Apart from this formal reason it isobvious that 0 <= i < n wouldn’t hold during the second loop iteration unless we reestablished it at the end of the first one, and that is just what the while rule requires.2.6. Derived RulesThe above rules don’t cover all kinds of statements allowed in C. However, missing C-statementscan be rewritten into a form that is semantically equivalent and covered by the Hoare rules.For example,switch (E) {case E1: Q1; break; ...case En: Qn; break;default: Q0; break;}is semantically equivalent toif (E == E1) {Q1} else ... if (E == En) {Qn} else {Q0}if E doesn’t have side-effects.
While the if-else form is usually slower in terms of executionspeed on a real computer, this doesn’t matter for verification purposes, which are separate fromexecution issues.7We would have to change the call to process(a,&i,&done) and the implementation of process appropriately. In this case we couldn’t rely on the above-mentioned assigns clause for process.19Similarly, for (P; Q; R) { S } can be re-expressed as P; while (Q) { S ; R }, and so on.It is then possible to derive a Hoare rule for each kind of statement not previously discussed, byapplying the classical rules to the corresponding re-expressed code fragment. However, we do notpresent these derived rules here.Although procedures cannot be re-expressed in the above way if they are (directly or mutually)recursive, it is still possible to derive Hoare rules for them.
This requires the finding of appropriate“procedure invariants” similar to loop invariants. Non-recursive procedures can, of course, just beinlined to make the classical Hoare rules applicable.Note that goto cannot be rewritten in the above way; in fact, programs containing goto statementscannot be verified with the Hoare Calculus. See [15] for a similar calculus that can deal witharbitrary flowcharts, and hence arbitrary jumps. In fact, Hoare’s work was based on that calculus.Later calculi inspired from Hoare’s work have been designed to re-integrate support for arbitraryjumps. Jessie only supports forward jumps.
However, in this tutorial, we will not discuss exampleprograms containing a goto.203. Non-mutating AlgorithmsIn this chapter, we consider non-mutating algorithms, i.e., algorithms that neither change theirarguments nor any objects outside their scope. This requirement can be formally expressed withthe following assigns clause:assigns \nothing;Each algorithm in this chapter therefore uses this assigns clause in its specification.The specifications of these algorithms are not very complex. Nevertheless, we have tried to arrangethem so that the earlier examples are simpler than the latter ones.
All algorithms work on onedimensional arrays (“ranges”).equal (Section 3.1 on Page 22) compares two ranges element-by-element.mismatch (Section 3.2 on Page 26) returns the smallest index where two ranges differ. Animplementation of equal using mismatch is introduced.find (Section 3.3 on Page 28) provides sequential or linear search and returns the smallestindex at which a given value occurs in a range. In Section 3.4, on Page 30, a predicate isintroduced in order to simplify the specification.find first of (Section 3.5, on Page 32) provides similar to find a sequential search, butunlike find it does not search for a particular value, but for the least index of a given rangewhich occurs in another range.adjacent find which can be used to find equal neighbors in an array (Section 3.6).count (Section 3.7, on Page 36) returns the number of occurrences of a given value in a range.Here we will employ some user-defined axioms to formally specify count.search (Section 3.8, on Page 38) finds a subsequence that is identical to a given sequence whencompared element-by-element and returns the position of the first occurrence.213.1.
The equal AlgorithmThe equal algorithm in the C++ Standard Library compares two generic sequences. For ourpurposes we have modified the generic implementation8 to that of an array of type value_type.The signature now reads:bool equal(const value_type* a, size_type n, const value_type* b);The function returns true if a[i] == b[i] holds for each 0 <= i < n.
Otherwise, equalreturns false.3.1.1. Formal Specification of equalThe ACSL specification of equal is shown in Listing 3.1. We discuss the specification now lineby line.1 /*@2requires IsValidRange(a, n);3requires IsValidRange(b, n);45assigns \nothing;67behavior all_equal:8assumes \forall integer i; 0 <= i < n ==> a[i] == b[i];9ensures \result;1011behavior some_not_equal:12assumes \exists integer i; 0 <= i < n && a[i] != b[i];13ensures !\result;1415complete behaviors;16disjoint behaviors;17 */18 bool equal(const value_type* a, size_type n, const value_type* b);Listing 3.1: Formal specification of equalLines 2–3 formalize the requirements that n is non-negative and that the pointers a and b pointto n contiguously allocated objects of type value_type (see also Section 1.3).Line 5 indicates that equal, as a non-mutating algorithm, does not modify any memory locationoutside its scope (see Page 21).The behavior all_equal applies if an element-wise comparison of the two ranges yields thatthey are equal, see Line 8.
In this case the function equal is expected to return true (Line 9).The behavior some_not_equal applies if there is at least one valid index i where the elements a[i] and b[i] differ (Line 12). In this case the function equal is expected to returnfalse (Line 13).8See http://www.sgi.com/tech/stl/equal.html.22Completeness and Disjointness of BehaviorsThe negation of the formula\forall integer i; 0 <= i < n ==> a[i] == b[i];in behavior all_equal is just the formula\exists integer i; 0 <= i < n && a[i] != b[i];in behavior some_not_equal. Therefore, these two behaviors complement each other.Line 15 in Listing 3.1 expresses the fact that for all ranges a and b that satisfy the preconditions ofthe contract (Lines 2 and 3) at least one of the specified named behaviors, in this case all_equaland some_not_equal, applies. Line 16 in Listing 3.1 formalizes the fact that for all ranges aand b that satisfy the preconditions of the contract (Lines 2 and 3) at most one of the specifiednamed behaviors, in this case all_equal and some_not_equal, applies.3.1.2.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
