ACSL Language Reference (811287), страница 6
Текст из файла (страница 6)
In fact, x denotes the effective parameter of isqrt calls, whichhas the same value interpreted in the pre-state as in the post-state.Example 2.19 The following function is given a contract to specify that it increments thevalue pointed to by the pointer given as argument.12345/*@ requires \valid (p);@ assigns *p;@ ensures *p == \old(*p) + 1;@*/void incrstar(int *p);The contract means that the function must be called with a pointer p that points to a safelyallocated memory location (see Section 2.7 for details on the \valid built-in predicate). Itdoes not modify any memory location but the one pointed to by p. 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:31CHAPTER 2.
SPECIFICATION LANGUAGE• 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 readability (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 ;@*/A 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 : ...@ ...@*/322.3. FUNCTION CONTRACTSExample 2.20 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.Example 2.21 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 isdesired, 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. that33CHAPTER 2. SPECIFICATION LANGUAGER ==> (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.2.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 that are also useful forthe \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 \empty342.3. FUNCTION CONTRACTStsetpred::=|||||||||||||\emptytset -> idtset . id* tset& tsettset [ tset ]term? .. term?\union ( tset (, tset)∗ )\inter ( tset (, tset)∗ )tset + tset( tset ){ tset | binders (; pred)?{ (tset (, tset)∗ )? }::=\subset ( tsettermempty setrangeunion of locationsintersection}set comprehensionimplicit singleton, tset)set inclusionFigure 2.7: Grammar for sets of terms• \union(s1 ,. . .,sn ) denotes the union of s1 ,s2 , .
. . and sn ;• \inter (s1 ,. . .,sn ) denotes the intersection of s1 ,s2 , . . . and sn ;• s1 +s2 denotes the set of x1 +x2 for each x1 ∈ s1 and x2 ∈ s2 ;• { t1 ,. . .,tn } is the set composed of the elements t1 , . . ., tn .• (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.22 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.23 The following function increments each value stored in a linked list.35CHAPTER 2. SPECIFICATION LANGUAGE1234struct 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.On 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 .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
