ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver (1185160), страница 6
Текст из файла (страница 6)
Finally, the ensures clausespecifies that the value *p is incremented by one.2.3.3Contracts with named behaviorsThe general form of a function contract contains several named behaviors (restricted to twobehaviors, in the following, for readability).123456789101112/*@ requires P;@ behavior b1 :@ assumes A1 ;@requires R1 ;@assigns L1 ;@ensures E1 ;@ behavior b2 :@ assumes A2 ;@requires R2 ;@assigns L2 ;@ensures E2 ;@*/The semantics of such a contract is as follows:• The caller of the function must guarantee that the call is performed in a state wherethe property P && (A1 ==> R1 ) && (A2 ==> R2 ) holds.• The called function returns a state where the properties \old(Ai ) ==> Ei hold for each i.• For each i, if the function is called in a pre-state where Ai holds, then each memorylocation of that pre-state that does not belong to the set Li is left unchanged in thepost-state.requires clauses in the behaviors are proposed mainly to improve readibility (to avoid someduplication of formulas), since the contract above is equivalent to the following simplifiedone:12345678910/*@ requires P && (A1 ==> R1 ) && (A2 ==> R2 );@ behavior b1 :@ assumes A1 ;@assigns L1 ;@ensures E2 ;@ behavior b2 :@ assumes A2 ;@assigns L2 ;@ensures E2 ;@*/31CHAPTER 2.
SPECIFICATION LANGUAGEA simple contract such as1/*@ requires P; assigns L; ensures E; */is actually equivalent to a single named behavior as follows:123456/*@ requires P;@ behavior <any name>:@ assumes \true;@assigns L;@ensures E;@*/Similarly, global assigns and ensures clauses are equivalent to a single named behavior.
Moreprecisely, the following contract1234567/*@ requires P;@ assigns L;@ ensures E;@ behavior b1 : ...@ behavior b2 : ...@ ...@*/is equivalent to123456789/*@ requires P;@ behavior <any name>:@ assumes \true;@assigns L;@ensures E;@ behavior b1 : ...@ behavior b2 : ...@ ...@*/Example 2.19 In the following, bsearch(t,n,v) searches for element v in array t betweenindices 0 and n-1.123456789101112/*@ 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, integer 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);The precondition requires array t to be allocated at least from indices 0 to n-1.
The twonamed behaviors correspond respectively to the successful behavior and the failing behavior.Since the function is performing a binary search, it requires the array t to be sorted inincreasing order: this is the purpose of the predicate named t_is_sorted in the assumes clauseof the behavior named failure.See 2.4.2 for a continuation of this example.322.3.
FUNCTION CONTRACTSExample 2.20 The following function illustrates the importance of different assigns clausesfor each behavior.1234567891011121314/*@ behavior p_changed:@ assumes n > 0;@requires \valid (p);@assigns *p;@ensures *p == n;@ behavior q_changed:@ assumes n <= 0;@requires \valid (q);@assigns *q;@ensures *q == n;@*/void f(int n, int *p, int *q) {if (n > 0) *p = n; else *q = n;}Its contract means that it assigns values pointed to by p or by q, conditionally on the signof n.Completeness of behaviorsIn a contract with named behaviors, it is not required that the disjunction of the Ai is true,i.e.
it is not mandatory to provide a “complete” set of behaviors. If such a condition isseeked, it is possible to add the following clause to a contract:/*@ ...@ complete behaviors b1 ,...,bn ;@*/It specifies that the set of behaviors b1 ,. . .,bn is complete i.e.
thatR ==> (A1 || A2 || ... || An )holds, where R is the precondition of the contract. The simplified version of that clause/*@ ...@ complete behaviors ;@*/means that all behaviors given in the contract should be taken into account.Similarly, it is not required that two distinct behaviors are disjoint. If desired, this can bespecified with the following clause:/*@ ...@ disjoint@*/behaviors b1 ,...,bn ;It means that the given behaviors are pairwise disjoint i.e. that, for all distinct i and j,R ==> ! (Ai && Aj )holds.
The simplified version of that clause/*@ ...@ disjoint@*/behaviors ;means that all behaviors given in the contract should be taken into account. Multiple completeand disjoint sets of behaviors can be given for the same contract.33CHAPTER 2. SPECIFICATION LANGUAGEtsetpreda::=|||||||||||||\emptyempty settset -> idtset . id* tset& tsettset [ tset ]term? .. term?\union ( tset (, tset)∗ )\inter ( tset (, tset)∗ )tset + tset( tset ){ tset | binders (; pred)?{ term }atermrangeunion of locationsintersection::=\subset ( tset, tset})set comprehensionexplicit singletonimplicit singletonset inclusionthe given term cannot itself be a setFigure 2.7: Grammar for sets of terms2.3.4Memory locations and sets of termsThere are several places where one needs to describe a set of memory locations: in assignsclauses of function contracts, or in loop assigns clauses (see section 2.4.2).
A memory locationis then any set of terms denoting a set of l-values. Moreover, a location given as argumentto an assigns clause must be a set of modifiable l-values, as described in Section A.1. Moregenerally, we introduce syntactic constructs to denote sets of terms which are also usefull for\separated predicate (see Section 2.7.2)The grammar for sets of terms is given in Figure 2.7. The semantics is given below, where sdenotes any tset.• \empty denotes the empty set.• a simple term denotes a singleton set.• s->id denotes the set of x->id for each x ∈ s.• s.id denotes the set of x.id for each x ∈ s.• *s denotes the set of *x for each x ∈ s.• &s denotes the set of &x for each x ∈ s.• s1 [s2 ] denotes the set of x1 [x2 ] for each x1 ∈ s1 and x2 ∈ s2 .• t1 ..
t2 denotes the set of integers between t1 and t2 , included. If t1 > t2 , this thesame as \empty• \union(s1 ,. . .,sn ) denotes the union of s1 ,s2 , . . . and sn ;• \inter (s1 ,. . .,sn ) denotes the intersection of s1 ,s2 , . . . and sn ;342.3. FUNCTION CONTRACTS• s1 +s2 denotes the set of x1 +x2 for each x1 ∈ s1 and x2 ∈ s2 ;• (s) denotes the same set as s;• { s | b ; P } denotes set comprehension, that is the union of the sets denoted by sfor each value b of binders satisfying predicate P (binders b are bound in both s and P).Note that assigns \nothing is equivalent to assigns \empty; it is left for convenience.Example 2.21 The following function sets to 0 each cell of an array.123456789/*@ requires \valid (t+(0..n-1));@ assigns t[0..n-1];@ assigns *(t+(0..n-1));@ assigns *(t+{ i | integer i ; 0 <= i < n });@*/void reset_array(int t[],int n) {int i;for (i=0; i < n; i++) t[i] = 0;}It is annotated with three equivalent assigns clauses, each one specifying that only the set ofcells {t[0],.
. .,t[n-1]} is modified.Example 2.22 The following function increments each value stored in a linked list.1234struct list {int hd;struct list *next;};56789101112// reachability in linked lists/*@ inductive reachable{L}(struct list *root, struct list *to) {@ case empty{L}: \forall struct list *l; reachable(l,l) ;@ case non_empty{L}: \forall struct list *l1,*l2;@\valid (l1) && reachable(l1->next,l2) ==> reachable(l1,l2) ;@ }*/1314151617181920// The requires clause forbids to give a circular list/*@ requires 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; }}The assigns clause specifies that the set of modified memory locations is the set of fields q->hdfor each pointer q reachable from p following next fields.
See Section 2.6.3 for details aboutthe declaration of the predicate reachable.2.3.5Default contracts, multiple contractsA C function can be defined only once but declared several times. It is allowed to annotateeach of these declarations with contracts. Those contracts are seen as a single contract withthe union of the requires clauses and behaviors.35CHAPTER 2. SPECIFICATION LANGUAGEC-compound-statement::={ declaration∗statement∗C-statement::=assertionassertion::=|/*@ assert pred ; *//*@ for id (, id)∗ : assert predassertion+}C-statement; */Figure 2.8: Grammar for assertionsOn the other hand, a function may have no contract at all, or a contract with missing clauses.Missing requires and ensures clauses default to \true . 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.2.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.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
