ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver, страница 8

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.28 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.12345678910/*@ 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 ;422.4.

STATEMENT ANNOTATIONS11121314151617181920212223}@ loop variant y;@*/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.29 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.30 Here is an example illustrating the use of LoopEntry and LoopCurrent12345678910void f (int n) {for (int i = 0; i < n; i++) {/*@ assert \at(i,LoopInit) == 0; */int j = 0;while (j++ < i) {/*@ assert \at(j,LoopInit) == 0; *//*@ assert \at(j,LoopCurrent) + 1 == j; */}}}2.4.4Statement contractsThe grammar for statement contracts is given in Figure 2.11. It is similar to function contracts, but without decreases clause.

Additionally, a statement contract may refer to enclosing43CHAPTER 2. SPECIFICATION LANGUAGEstatement::=/*@ statement-contract*/ statement::=( for id (,simple-clause-stmt∗requires-clause ∗named-behavior-stmt∗::=|simple-clauseallocation-clauseabrupt-clause-stmtnamed-behavior-stmt::=behavior idbehavior-body-stmt::=assumes-clause ∗requires-clause ∗ simple-clause-stmt∗statement-contractsimple-clause-stmtid)∗:)?|: behavior-body-stmtFigure 2.11: Grammar for statement contractsnamed behaviors, with the form for id:.... Such contracts are only valid for the corresponding 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 begining of the annoted statement andleading to a goto jumping out of it, should be part of its assigns clause.Example 2.31 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).442.5. TERMINATION2.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.24).Example 2.32 The clause loop variant u-l; can be added to the loop annotations of theexample 2.23.

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.33 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;45CHAPTER 2.

SPECIFICATION LANGUAGE@*/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.

We call cluster a set of mutually recursive functionswhich is a strongly connected component of the call graph. Within each cluster, each functionmust be annotated with a decreases clause with the same relation R (syntactically). Then,in the body of any function f of that cluster, any recursive call to a function g must occurin a state where the measure attached to g is smaller (w.r.t R) than the measure of f in thepre-state of f.

This also applies when g is f itself.Example 2.34 Here are the classical factorial and Fibonacci functions:12345678/*@ requires n <= 12;@ decreases n;@*/int fact(int n) {if (n <= 1) return 1;return n * fact(n-1);}91011121314//@ decreases n;int fib(int n) {if (n <= 1) return 1;return fib(n-1) + fib(n-2);}Example 2.35 This example illustrates mutual recursion:12345678/*@requires n>=0;decreases n;*/int even(int n) {if (n == 0) return 1;return odd(n-1);}9462.6.

LOGIC SPECIFICATIONS1011121314151617/*@requires x>=0;decreases x;*/int odd(int x) {if (x == 0) return 0;return even(x-1);}2.5.4Non-terminating functionsExperimentalThere are cases where a function is not supposed to terminate. For instance, the main functionof a reactive program might be a while (1) which indefinitely waits for an event to process.More generally, a function can be expected to terminate only if some preconditions are met.In those cases, a terminates clause can be added to the contract of the function, under thefollowing form://@ terminates p;The semantics of such a clause is as follows: if p holds, then the function is guaranteed toterminate (more precisely, its termination must be proved).

If such a clause is not present(and in particular if there is no function contract at all), it defaults to terminates \true;that is the function is supposed to always terminate, which is the expected behavior of mostfunctions.Note that nothing is specified for the case where p does not hold: the function may terminateor not. In particular, terminates \false ; does not imply that the function loops forever. Apossible specification for a function that never terminates is the following:1234/*@ ensures \false ;terminates \false ;*/void f() { while(1); }Example 2.36 A concrete example of a function that may not always terminate is theincr_list function of example 2.22. In fact, The following contract is also acceptable forthis function:123456782.6// this time, the specification accepts circular lists, but does not ensure// that the function terminates on them (as a matter of fact, it does not)./*@ terminates reachable(p,\null);@ assigns { q->hd | struct list *q ; reachable(p,q) } ;@*/void incr_list(struct list *p) {while (p) { p->hd++ ; p = p->next; }}Logic specificationsThe language of logic expressions used in annotations can be extended by declarations of newlogic types, and new constants, logic functions and predicates.