ACSL Language Reference (811287), страница 13
Текст из файла (страница 13)
More generally,the visibility in abrupt clauses of predefined logic labels (presented in Section 2.4.3) is thesame as in ensures clauses.For the returns case, the \result construct is allowed (if the function is not returning void )and is bound to the returned value.Example 2.54 The following example illustrates each abrupt clause of statement contracts.1int f(int x) {23while (x > 0) {4567891011121314151617181920}/*@ breaks x % 11 == 0 && x == \old(x);@ continues (x+1) % 11 != 0 && x % 7 == 0 && x == \old(x)-1;@ returns ( \result +2) % 11 != 0 && (\result+1) % 7 != 0@&& \result % 5 == 0 && \result == \old(x)-2;@ ensures (x+3) % 11 != 0 && (x+2) % 7 != 0 && (x+1) % 5 != 0@&& x == \old(x)-3;@*/{if (x % 11 == 0) break;x--;if (x % 7 == 0) continue;x--;if (x % 5 == 0) return x;x--;}67CHAPTER 2.
SPECIFICATION LANGUAGE2122}return x;The exits clause can be used in both function and statement contracts to give behavioralproperties to the main function or to any function that may exit the program, e.g. by callingthe exit function.In such clauses, \old(e) is allowed and denotes the value of e in the pre-state of the functionor statement, and \exit_status is bound to the return code, e.g. the value returned by main orthe argument passed to exit. The construct \exit_status can be used only in exits, assignsand allocates clauses.
On the contrary, \result cannot be used in exits clauses.Example 2.55 Here is a complete specification of the exit function which performs an unconditional exit of the main function:12345/*@ assigns \nothing;@ ensures \false ;@ exits \exit_status == status;@*/void exit(int status);67int status;891011121314151617/*@ assigns status;@ exits !cond && \exit_status == 1 && status == val;@*/void may_exit(int cond, int val) {if (! cond) {status = val;exit(1);}}Note that the specification of the may_exit function is incomplete since it allows modificationsof the variable status when no exit is performed. Using behaviors, it is possible to distinguishbetween the exit case and the normal case, as in the following specification:89101112131415161718/*@ behavior no_exit :@ assumes cond;@assigns \nothing;@ exits \false ;@ behavior no_return :@ assumes !cond;@assigns status;@ exits \exit_status == 1 && status == val;@ensures \false ;@*/void may_exit(int cond, int val) ;Contrary to ensures clauses, assigns , allocates and frees clauses of function and statementcontracts constrain the post-state even when the annotated function and statement terminatesrespectively abruptly.
This is shown in example 2.55 for a function contract.682.10. DEPENDENCIES INFORMATIONassigns-clause::=|assigns location (, location)∗ (\from locations )?assigns term \from locations = term ;;Figure 2.24: Grammar for dependencies information2.10Dependencies informationExperimentalAn extended syntax of assigns clauses, described in Figure 2.24 allows to specify data dependencies and functional expressions.Such a clause indicates that the assigned values can only depend upon the locations mentionedin the \from part of the clause. Again, this is an over-approximation: all of the locationsinvolved in the computation of the modified values must be present, but some of locationsmight not be used in practice. If the \from clause is absent, all of the locations reachable atthe given point of the program are supposed to be used. Moreover, for a single location, it ispossible to give the precise relation between its final value and the value of its dependencies.This expression is evaluated in the pre-state of the corresponding contract.Example 2.56 The following example is a variation over the array_sum function in example 2.44, in which the values of the array are added to a global variable total.1double total = 0.0;234567891011/*@ requires n >= 0 && \valid(t+(0..n-1)) ;@ assigns total\from t[0..n-1] = total + \sum(0,n-1,\lambda int k; t[k]);@*/void array_sum(double t[],int n) {int i;for (i=0; i < n; i++) total += t[i];return ;}Example 2.57 The composite element modifier operators can be useful for writing such functional expressions.1struct buffer { int pos ; char buf[80]; } line;234567891011/*@ requires 80 > line.pos >= 0 ;@ assigns line@ \from line ={ line \with .buf ={ line.buf \with [line.pos] = (char)'\0' } };@*/void add_eol() {line.buf[line.pos] = '\0' ;}2.11Data invariants69CHAPTER 2.
SPECIFICATION LANGUAGEdeclaration::=/*@ data-inv-decldata-inv-decl::=data-invariantdata-invariant::=inv-strength? globalid : pred ;type-invariant::=inv-strength? type invariantid ( C-type-name id ) = predinv-strength::=weak |*/| type-invariantinvariant;strongFigure 2.25: Grammar for declarations of data invariantsData invariants are properties on data that are supposed to hold permanently during thelifetime of these data. In ACSL, we distinguish between:• global invariants and type invariants: the former only apply to specified global variables,whereas the latter are associated to a static type, and apply to any variables of thecorresponding type;• strong invariants and weak invariants: strong invariants must be valid at any timeduring program execution (more precisely at any sequence point as defined in the Cstandard), whereas weak invariants must be valid at function boundaries (functionentrance and exit) but can be violated in between.The syntax for declaring data invariants is given in Figure 2.25.
The strength modifierdefaults to weak.Example 2.58 In the following example, we declare1. a weak global invariant a_is_positive which specifies that global variable a should remain positive (weakly, so this property might be violated temporarily between functionscalls);2. a strong type invariant for variables of type temperature;3.
a weak type invariant for variables of type struct S.12int a;//@ global invariant a_is_positive: a >= 0 ;34567typedef double temperature;/*@ strong type invariant temp_in_celsius(temperature t) =@ t >= -273.15 ;@*/89101112struct S {int f;};//@ type invariant S_f_is_positive(struct S s) = s.f >= 0 ;702.11.
DATA INVARIANTS2.11.1SemanticsThe distinction between strong and weak invariants has to do with the sequence points wherethe property is supposed to hold. The distinction between global and type invariants has todo with the set of values on which they are supposed to hold.• Weak global invariants are properties which apply to global data and hold at anyfunction entrance and function exit.• Strong global invariants are properties which apply to global data and hold at any stepduring execution (starting after initialization of these data).• A weak type invariant on type τ must hold at any function entrance and exit, andapplies to any global variable or formal parameter with static type τ .
If the result ofthe function is of type τ , the result must also satisfy its weak invariant at function exit.However, it says nothing about fields, array elements, memory locations, etc. of typeτ.• A strong type invariant on type τ must hold at any step during execution, and appliesto any global variable, local variable, or formal parameter with static type τ . If theresult of the function has type τ , the result must also satisfy its strong invariant atfunction exit. Again, it says nothing about fields, array elements, memory locations,etc.
of type τ .Example 2.59 The following example illustrates the use of a data invariant on a local staticvariable.123456void out_char(char c) {static int col = 0;//@ global invariant I : 0 <= col <= 79;col++;if (col >= 80) col = 0;}Example 2.60 Here is a longer example, the famous Dijkstra’s Dutch flag algorithm.1234typedef enum { BLUE, WHITE, RED } color;/*@ type invariant isColor(color c) =@ c == BLUE || c == WHITE || c == RED ;@*/5678910111213141516/*@ predicate permut{L1,L2}(color@ \at( \valid (t1+(0..n)),L1) &&@ \numof(0,n,\lambda integer i;@ \numof(0,n,\lambda integer i;@ &&@ \numof(0,n,\lambda integer i;@ \numof(0,n,\lambda integer i;@ &&@ \numof(0,n,\lambda integer i;@ \numof(0,n,\lambda integer i;@*/*t1, color *t2, integer n) =\at(\valid(t2+(0..n)),L2) &&\at(t1[i],L1) == BLUE) ==\at(t2[i],L2) == BLUE)\at(t1[i],L1) == WHITE) ==\at(t2[i],L2) == WHITE)\at(t1[i],L1) == RED) ==\at(t2[i],L2) == RED);1771CHAPTER 2.
SPECIFICATION LANGUAGE1819202122232425262728293031323334/*@ requires \valid (t+i) && \valid(t+j);@ assigns t[i],t[j];@ ensures t[i] == \old(t[j]) && t[j] == \old(t[i]);@*/void swap(color t[], int i, int j) {int tmp = t[i];t[i] = t[j];t[j] = tmp;}typedef struct flag {int n;color *colors;} flag;/*@ type invariant is_colored(flag f) =@ f.n >= 0 && \valid(f.colors+(0..f.n-1)) &&@\forall integer k; 0 <= k < f.n ==> isColor(f.colors[k]) ;@*/3536373839/*@ predicate isMonochrome{L}(color *t, integer i, integer j,@color c) =@\forall integer k; i <= k <= j ==> t[k] == c ;@*/40414243444546474849505152535455565758596061626364656667686970717273/*@ assigns f.colors[0..f.n-1];@ ensures@\exists integer b, integer r;@isMonochrome(f.colors,0,b-1,BLUE) &&@isMonochrome(f.colors,b,r-1,WHITE) &&@isMonochrome(f.colors,r,f.n-1,RED) &&@permut{Old,Here}(f.colors,f.colors,f.n-1);@*/void dutch_flag(flag f) {color *t = f.colors;int b = 0;int i = 0;int r = f.n;/*@ loop invariant@ ( \forall integer k; 0 <= k < f.n ==> isColor(t[k])) &&@ 0 <= b <= i <= r <= f.n &&@ isMonochrome(t,0,b-1,BLUE) &&@ isMonochrome(t,b,i-1,WHITE) &&@ isMonochrome(t,r,f.n-1,RED) &&@ permut{Pre,Here}(t,t,f.n-1);@ loop assigns b,i,r,t[0 ..
f.n-1];@ loop variant r - i;@*/while (i < r) {switch (t[i]) {case BLUE:swap(t, b++, i++);break;case WHITE:i++;break;case RED:swap(t, --r, i);722.11. DATA INVARIANTSbreak;74757677}2.11.2}}Model variables and model fieldsA model variable is a variable introduced in the specification with the keyword model. Its typemust be a logic type. Analogously, types may have model fields. These are used to provideabstract specifications to functions whose concrete implementation must remain private.The precise syntax for declaring model variables and fields is given in Figure 2.26. It ispresented as additions to the regular C grammar for declarationsInformal semantics of model variables is as follows.• Model variables can only appear in specifications.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
