ACSL Language Reference (811287), страница 8
Текст из файла (страница 8)
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;3456while (y > 0) {x++;//@ invariant 0 < x < 11;41CHAPTER 2. SPECIFICATION LANGUAGE789}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 [13], Section A11.1).Default logic labelsThere are seven predefined logic labels: Pre, Here, Old, Post, LoopEntry, LoopCurrent andInit. \old(e) is in fact syntactic sugar for \at(e,Old).• 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.422.4.
STATEMENT ANNOTATIONSterm::=\at ( term, label-id)pred::=\at ( pred, label-id)label-id::=||Here | Old | Pre | PostLoopEntry | LoopCurrent |Init |idFigure 2.11: Grammar for at construct• 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.• The label Init is visible in all statement annotations and contracts. It refers to thestate just before the call to the main function, once the global data have been initialized.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.
In such clauses formal parametersalways refer implicitly to the label Pre, and any \at construct can modify the interpretationof formal parameters.No logic label is visible in global logic declarations such as lemmas, axioms, definition ofpredicate or logic functions. When such an annotation needs to refer to a given memorystate, it has to be given a label binder: this is described in Section 2.6.9.Example 2.29 The code below implements the famous extended Euclid’s algorithm for computing the greatest common divisor of two integers x and y, while computing at the same timetwo Bézout coefficients p and q such that p × x + q × y = gcd(x, y). The loop invariant forthe Bézout property needs to refer to the value of x and y in the pre-state of the function.1234567891011/*@ requires x >= 0 && y >= 0;@ behavior bezoutProperty:@ensures (*p)*x+(*q)*y == \result;@*/int extended_Euclid(int x, int y, int *p, int *q) {int a = 1, b = 0, c = 0, d = 1;/*@ loop invariant x >= 0 && y >= 0 ;@ for bezoutProperty: loop invariant@a*\at(x,Pre)+b*\at(y,Pre) == x &&@c*\at(x,Pre)+d*\at(y,Pre) == y ;@ loop variant y;43CHAPTER 2.
SPECIFICATION LANGUAGE121314151617181920212223}@*/while (y > 0) {int r = x % y;int q = x / y;int ta = a, tb = b;x = y; y = r;a = c; b = d;c = ta - c * q; d = tb - d * q;}*p = a; *q = b;return x;Example 2.30 Here is a toy example illustrating tricky issues with \at and labels:12int i;int t[10];345//@ ensures 0 <= \result <= 9;int any();678910111213141516/*@ assigns i,t[\at(i,Post)];@ ensures@ t[i] == \old(t[\at(i,Here)]) + 1;@ ensures@\let j = i; t[j] == \old(t[j]) + 1;@*/void f() {i = any();t[i]++;}The two ensures clauses are equivalent.
The simpler clause t[i] == \old(t[i]) + 1 would bewrong because in \old(t[i]), i denotes the value of i n the pre-state.Also, the assigns clause i,t[i] would be wrong too because again in t[i], the value of i inthe pre-state is considered.Example 2.31 Here is an example illustrating the use of LoopEntry and LoopCurrent12345678910void f (int n) {for (int i = 0; i < n; i++) {/*@ assert \at(i,LoopEntry) == 0; */int j = 0;while (j++ < i) {/*@ assert \at(j,LoopEntry) == 0; *//*@ assert \at(j,LoopCurrent) + 1 == j; */}}}2.4.4Statement contractsThe grammar for statement contracts is given in Figure 2.12.
It is similar to function contracts, but without a decreases clause. Additionally, a statement contract may refer to en-442.5. TERMINATIONstatement::=/*@ statement-contract( for id (,requires-clause ∗simple-clause-stmt∗ named-behavior-stmt∗completeness-clause ∗::=simple-clausenamed-behavior-stmt::=behavior idbehavior-body-stmt::=assumes-clause ∗requires-clause ∗ simple-clause-stmt∗simple-clause-stmtaid)∗*/ statement::=statement-contracta|:)?abrupt-clause-stmt: behavior-body-stmtempty contracts are forbiddenFigure 2.12: Grammar for statement contractsclosing named behaviors, with the form for id:....
Such contracts are only valid for thecorresponding behaviors, in particular only under the corresponding assumes clause.The ensures clause does not constrain the post-state when the annotated statement is terminated by a goto jumping out of it, by a break , continue or return statement, or by a call to theexit function. To specify such behaviors, abrupt clauses (described in Section 2.9) need tobe used.On the other hand, it is different with assigns clauses.
The locations having their valuemodified during the path execution, starting at the beginning of the annotated statementand leading to a goto jumping out of it, should be part of its assigns clause.Example 2.32 The clause assigns \nothing; does not hold for that statement, even if theclause ensures x==\old(x); holds:12345678/*@ assigns x;@ ensures x==\old(x);@*/if (c) {x++;goto L;}L: ...Allocation-clauses allow to specify which memory location is dynamically allocated or deallocated by the annotated statement from the heap; they are defined later in Section 2.7.3.2.5TerminationThe property of termination concerns both loops and recursive function calls. Terminationis guaranteed by attaching a measure function to each loop (aspect already addressed inSection 2.4.2) and each recursive function.
By default, a measure is an integer expression,and measures are compared using the usual ordering over integers (Section 2.5.1). It is alsopossible to define measures into other domains and/or using a different ordering relation(Section 2.5.2).45CHAPTER 2. SPECIFICATION LANGUAGE2.5.1Integer measuresFunctions are annotated with integer measures with the syntax//@ decreases e;and loops are annotated similarly with the syntax//@ loop variant e;where the logic expression e has type integer . For recursive calls, or for loops, this expressionmust decrease for the relation R defined byR(x,y) <==> x > y && x >= 0.In other words, the measure must be a decreasing sequence of integers which remain nonnegative, except possibly for the last value of the sequence (See example 2.25).Example 2.33 The clause loop variant u-l; can be added to the loop annotations of theexample 2.24.
The measure u-l decreases at each iteration, and remains nonnegative, exceptat the last iteration where it may become negative.161718@ ...@ loop variant u-l; */while ...2.5.2General measuresMore general measures on other types can be provided, using the keyword for . For functionsit becomes//@ decreases e for R;and for loops//@ loop variant e for R;In those cases, the logic expression e has some type τ and R must be relation on τ , that is abinary predicate declared (see Section 2.6 for details) as//@ predicate R(τ x, τ y) · · ·Of course, to guarantee termination, it must be proved that R is a well-founded relation.Example 2.34 The following example illustrates a variant annotation using a pair of integers, ordered lexicographically.12//@ ensures \result >= 0;int dummy();34//@ type intpair = (integer,integer);5678910/*@ predicate lexico(intpair p1, intpair p2) =@\let (x1,y1) = p1 ;@\let (x2,y2) = p2 ;@x1 < x2 && 0 <= x2 ||@x1 == x2 && 0 <= y2 && y1 < y2;462.5.
TERMINATION@*/1112131415161718//@ requires x >= 0 && y >= 0;void f(int x,int y) {/*@ loop invariant x >= 0 && y >= 0;@ loop variant (x,y) for lexico;@*/while (x > 0 && y > 0) {19202122232425}2.5.3}if (dummy()) {x--; y = dummy();}else y--;Recursive function callsThe precise semantics of measures on recursive calls, especially in the general case of mutuallyrecursive functions, is given as follows.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
