ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver (1185160), страница 7
Текст из файла (страница 7)
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.362.4. STATEMENT ANNOTATIONSstatement::=||/*@ loop-annot */while ( C-expression ) C-statement/*@ loop-annot */for ( C-expression ; C-expression ; C-expressionC-statement/*@ loop-annot */do C-statementwhile ( C-expression) ;loop-annot::=loop-clause ∗ loop-behavior ∗loop-variant?loop-clause::=|loop-invariant | loop-assignsloop-allocationloop-invariant::=looploop-assigns::=loop assigns locationsloop-behavior::=for idloop-variant::=|looploopinvariant;pred(, id)∗;: loop-clause ∗variant termvariant term);for id;annotation for behaviovariant for relation idFigure 2.9: Grammar for loop annotationsLoop 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;– 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, which37CHAPTER 2.
SPECIFICATION LANGUAGEin 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 member of L.Loop behaviorsA loop annotation preceded by for id_1,.
. .,id_k: is similar as above, but applies only forbehaviors id_1,. . .,id_k of the current function, hence in particular holds only under theassumption of their assumes clauses.Remarks• 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 member of L can be assigned between theend of the previous iteration and the exit statement.Example 2.23 Here is a continuation of example 2.19.
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;}382.4.
STATEMENT ANNOTATIONSassertion::=|/*@ invariant pred ; *//*@ for id (, id)∗ : invariantpred; */Figure 2.10: Grammar for general inductive invariantsLoop 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.24123456void 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.25 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;}39CHAPTER 2. SPECIFICATION LANGUAGEMore 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.26 Here is a program annotated with an invariant inside the loop body:12345678910111213141516/*@ 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;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.27 The program12int x = 0;int y = 10;3456789/*@ loop invariant 0 <= x < 11;@*/while (y > 0) {x++;y--;}402.4.
STATEMENT ANNOTATIONSis not correctly annotated, even if it is true that x remains smaller than 11 during the execution. This is because it is not true that the property x<11 is preserved by the executionof x++ ; y--;. A correct loop invariant could be 0 <= x < 11 && x+y == 10. It holds at loopentrance and is preserved (under the assumption of the loop condition y>0).Similarly, the following general invariants are not inductive:12int x = 0;int y = 10;3456789while (y > 0) {x++;//@ invariant 0 < x < 11;y--;//@ invariant 0 <= y < 10;}since 0 <= y < 10 is not a consequence of hypothesis 0 < x < 11 after executing y--; and0 < x < 11 cannot be deduced from 0 <= y < 10 after looping back through the condition y>0and executing x++.
Correct invariants could be:1234562.4.3while (y > 0) {x++;//@ invariant 0 < x < 11 && x+y == 11;y--;//@ invariant 0 <= y < 10 && x+y == 10;}Built-in construct \atStatement annotations usually need another additional construct \at(e,id) referring to thevalue of the expression e in the state at label id. In particular, for a C array of int , t,\at(t,id) is a logical array whose content is the same as the one of t in state at label id. Itis thus very different from \at((int *)t,id), which is a pointer to the first element of t (andstays the same between the state at id and the current state).
Namely, if t[0] has changedsince id, we have \at(t,id)[0] != \at((int *)t,id)[0].The label id can be either a regular C label, or a label added within a ghost statement asdescribed in Section 2.12. This label must be declared in the same function as the occurrenceof \at(e,id), but unlike gotos, more restrictive scoping rules must be respected:• the label id must occur before the occurrence of \at(e,id) in the source;• the label id must not be inside an inner block.These rules are exactly the same rules as for the visibility of local variables within C statements (see [14], Section A11.1).Default logic labelsThere are six predefined logic labels: Pre, Here, Old, Post, LoopEntry and LoopCurrent. \old(e)is in fact syntactic sugar for \at(e,Old).41CHAPTER 2. SPECIFICATION LANGUAGE• The label Here is visible in all statement annotations, where it refers to the statewhere the annotation appears; and in all contracts, where it refers to the pre-state forthe requires , assumes, assigns , variant , terminates , clauses and the post-state for otherclauses.
It is also visible in data invariants, presented in Section 2.11.• The label Old is visible in assigns and ensures clauses of all contracts (both for functionsand for statement contracts described below in Section 2.4.4), and refers to the pre-stateof this contract.• The label Pre is visible in all statement annotations, and refers to the pre-state of thefunction it occurs in.• The label Post is visible in assigns and ensures clauses of all contracts, and it refers tothe post-state.• The label LoopEntry is visible in loop annotations and all annotations related to astatement enclosed in a loop.
It refers to the state just before entering that loopfor the first time –but after initialization took place in the case of a for loop, as forloop invariant (section 2.4.2). When LoopEntry is used in a statement enclosed in nestedloops, it refers to the innermost loop containing that statement.• The label LoopCurrent is visible in loop annotations and all other annotations relatedto a statement enclosed in a loop. It refers to the state at the beginning of the currentstep of the loop (see section 2.4.2 for more details on what constitutes a loop step inpresence of side-effects in the condition). When LoopCurrent is used in a statementenclosed in nested loops, it refers to the innermost loop containing that statement.Inside loop annotations, the labels LoopCurrent and Here are equivalent, except inside clausesloop frees (see section 2.7.3) where Here is equivalent to LoopEntry.There is one particular case for assigns and ensures clauses of function contracts where formalparameters of functions cannot refer to the label Post.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
