ACSL Language Reference (811287), страница 7
Текст из файла (страница 7)
If no assigns clause is given, it remainsunspecified. If the function under consideration has only a declaration but no body, thenit means that it potentially modifies “everything”, hence in practice it will be impossible toverify anything about programs calling that function; in other words giving it a contract isin practice mandatory. On the other hand, if that function has a body, giving no assignsclause means in practice that it is left to tools to compute an over-approximation of the setsof assigned locations.2.4Statement annotationsAnnotations on C statements are of three kinds:• Assertions: allowed before any C statement or at end of blocks.• Loop annotations: invariant , assigns clause, variant ; allowed before any loop statement:while , for , and do ... while.• Statement contracts: allowed before any C statement, specifying their behavior in asimilar manner to C function contracts.362.4.
STATEMENT ANNOTATIONSC-compound-statement::={ declaration∗statement∗C-statement::=assertionassertion::=|/*@ assert pred ; *//*@ for id (, id)∗ : assert predassertion+}C-statement; */Figure 2.8: Grammar for assertions2.4.1AssertionsThe syntax of assertions is given in Figure 2.8, as an extension of the grammar of C statements.• assert P means that P must hold in the current state (the sequence point where theassertion occurs).• The variant for id1 ,. . .,idk : assert P associates the assertion to the named behaviorsidi , each of them being a behavior identifier for the current function (or a behavior ofan enclosing block as defined later in Section 2.4.4). It means that this assertion musthold only for the considered behaviors.2.4.2Loop annotationsThe syntax of loop annotations is given in Figure 2.9, as an extension of the grammar of Cstatements.
Loop-allocation clauses allow to specify which memory location is dynamicallyallocated or deallocated by a loop from the heap; they are defined later in Section 2.7.3.Loop invariants and loop assignsThe semantics of loop invariants and loop assigns is defined as follows: a simple loop annotation of the form1234/*@ loop invariant I;@ loop assigns L;@*/...specifies that the following conditions hold.• The predicate I holds before entering the loop (in the case of a for loop, this meansright after the initialization expression).• The predicate I is an inductive invariant, that is if I is assumed true in some statewhere the condition c is also true, and if execution of the loop body in that state endsnormally at the end of the body or with a continue statement, I is true in the resultingstate. If the loop condition has side effects, these are included in the loop body in asuitable way:– for a while (c) s loop, I must be preserved by the side-effects of c followed by s;– for a for (init;c;step) s loop, I must be preserved by the side-effects of c followedby s followed by step;37CHAPTER 2.
SPECIFICATION LANGUAGEstatement::=||/*@ loop-annot */while ( C-expression)C-statement/*@ loop-annot */for ( C-expression ;C-expression ;C-expression )C-statement/*@ loop-annot */do C-statementwhile ( C-expression ) ;a::=loop-clause ∗ loop-behavior ∗loop-variant?loop-clause::=|loop-invariant |loop-allocationloop-invariant::=looploop-assigns::=loop assigns locationsloop-behavior::=for idloop-variant::=|looplooploop-annotainvariantloop-assigns;pred(, id)∗;: loop-clause +variant termvariant term;for id;annotation for behavior idvariant for relation idempty loop annotations are forbiddenFigure 2.9: Grammar for loop annotations– for a do s while (c); loop, I must be preserved by s followed by the side-effects ofc.Note that if c has side-effects, the invariant might not be true at the exit of the loop:the last “step” starts from a state where I holds, performs the side-effects of c, whichin the end evaluates to false and exits the loop.
Likewise, if a loop is exited through abreak statement, I does not necessarily hold, as side effects may occur between the laststate in which I was supposed to hold and the break statement.• At any loop iteration, any location that was allocated before entering the loop, and isnot member of L (interpreted in the current state) has the same value as before enteringthe loop. In fact, the loop assigns clause specifies an inductive invariant for the locationsthat are not members of L.Loop behaviorsA loop annotation preceded by for id_1,.
. .,id_k: is similar to the above, but applies onlyfor behaviors id_1,. . .,id_k of the current function, hence in particular holds only under theassumption of their assumes clauses.Remarks382.4. STATEMENT ANNOTATIONS• The \old construct is not allowed in loop annotations. The \at form should be used torefer to another state (see Section 2.4.3).• When a loop exits with break or return or goto, it is not required that the loop invariantholds. In such cases, locations that are not members of L can be assigned between theend of the previous iteration and the exit statement.• If no loop assigns clause is given, assignments remain unspecified.
It is left to tools tocompute an over-approximation of the sets of assigned locations.Example 2.24 Here is a continuation of example 2.20. Note the use of a loop invariantassociated to a function behavior.12345678910111213141516171819202122232425/*@ requires n >= 0 && \valid(t+(0..n-1));@ assigns \nothing;@ ensures -1 <= \result <= n-1;@ behavior success:@ensures \result >= 0 ==> t[\result] == v;@ behavior failure:@ assumes t_is_sorted : \forall integer k1, int k2;@0 <= k1 <= k2 <= n-1 ==> t[k1] <= t[k2];@ensures \result == -1 ==>@\forall integer k; 0 <= k < n ==> t[k] != v;@*/int bsearch(double t[], int n, double v) {int l = 0, u = n-1;/*@ loop invariant 0 <= l && u <= n-1;@ for failure: loop invariant@\forall integer k; 0 <= k < n && t[k] == v ==> l <= k <= u;@*/while (l <= u ) {int m = l + (u-l)/2; // better than (l+u)/2if (t[m] < v) l = m + 1;else if (t[m] > v) u = m - 1;else return m;}return -1;}Loop variantsOptionally, a loop annotation may include a loop variant of the form/*@ loop variant m; */where m is a term of type integer .The semantics is as follows: for each loop iteration that terminates normally or with continue ,the value of m at end of the iteration must be smaller that its value at the beginning of theiteration.
Moreover, its value at the beginning of the iteration must be nonnegative. Notethat the value of m at loop exit might be negative. It does not compromise termination ofthe loop. Here is an example:Example 2.2539CHAPTER 2. SPECIFICATION LANGUAGEassertion::=|/*@ invariant pred ; *//*@ for id (, id)∗ : invariantpred; */Figure 2.10: Grammar for general inductive invariants123456void f(int x) {//@ loop variant x;while (x >= 0) {x -= 2;}}It is also possible to specify termination orderings other than the usual order on integers,using the additional for modifier. This is explained in Section 2.5.General inductive invariantsIt is actually allowed to pose an inductive invariant anywhere inside a loop body. For example,it makes sense for a do s while (c); loop to contain an invariant right after statement s. Suchan invariant is a kind of assertion, as shown in Figure 2.10.Example 2.26 In the following example, the natural invariant holds at this point (\max and\lambda are introduced later in Section 2.6.7).
It would be less convenient to set an invariantat the beginning of the loop.123456789101112/*@ requires n > 0 && \valid(t+(0..n-1));@ ensures \result == \max(0,n-1,(\lambda integer k ; t[k]));@*/double max(double t[], int n) {int i = 0; double m,v;do {v = t[i++];m = v > m ? v : m;/*@ invariant m == \max(0,i-1,(\lambda integer k ; t[k])); */} while (i < n);return m;}More generally, loops can be introduced by gotos.
As a consequence, such invariants mayoccur anywhere inside a function’s body. The meaning is that the invariant holds at thatpoint, much like an assert . Moreover, the invariant must be inductive, i.e. it must bepreserved across a loop iteration. Several invariants are allowed at different places in a loopbody. These extensions are useful when dealing with complex control flows.Example 2.27 Here is a program annotated with an invariant inside the loop body:12345/*@ requires n > 0;@ ensures \result == \max(0,n-1,\lambda integer k; t[k]);@*/double max_array(double t[], int n) {double m; int i=0;402.4. STATEMENT ANNOTATIONS678910111213141516}goto L;do {if (t[i] > m) { L: m = t[i]; }/*@ invariant@ 0 <= i < n && m == \max(0,i,\lambda integer k; t[k]);@*/i++;}while (i < n);return m;The control-flow graph of the code is as followsi←0m < t[i]m ← t[i]dom ≥ t[i]invi←i+1i<ni≥nThe invariant is inductively preserved by the two paths that go from node “inv” to itself.Example 2.28 The program12int x = 0;int y = 10;3456789/*@ loop invariant 0 <= x < 11;@*/while (y > 0) {x++;y--;}is not correctly annotated, even if it is true that x remains smaller than 11 during the execution.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
