ACSL Language Reference (811287), страница 12

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 12)

POINTERS AND PHYSICAL ADDRESSING2627282930313233343536373839/*@ frees p;@ behavior deallocation:@ assumes p!=\null;@requires \freeable (p);@assigns heap_status;@ensures \allocable (p);@ behavior no_deallocation:@ assumes p==\null;@assigns \nothing;@frees\nothing;@ complete behaviors ;@ disjoint behaviors ;@*/void free(void *p);The behaviors named allocation and deallocation do not need an allocation clause. Forexample, the allocation constraint of the allocation behavior is given by the clause allocates\result of the anonymous behavior of the malloc function contract. To set a stronger constraint into the behavior named no_allocation, the clause allocates \nothing should be given.Allocation clauses for loop annotationsLoop annotations are complemented by similar clauses allowing to specify which memory location is dynamically allocated or deallocated by a loop.

The grammar for those constructionsis given on Figure 2.21.The clauses loop allocates and loop frees are tied together. The simple loop annotation/*@ loop frees P1 ,P2 ,...;@ loop allocates Q1 ,Q2 ,...; */means that any memory address that does not belong to the union of sets of terms Pi and Qihas the same allocation status in the current state than before entering the loop. The onlydifference between these two clauses is that sets Pi are evaluated in the state before enteringthe loop (label LoopEntry), and Qi are evaluated in the current loop state (label LoopCurrent).Namely, as for loop assigns , loop annotations loop frees and loop allocates define a loopinvariant.More precisely, the following loop annotation://@ loop allocates Q1 ,...,Qn ; */is equivalent to the loop invariant:\forall char* p;\separated (\union(Q1 ,.

. .,Qn ),p) ==>(\base_addr{Here}(p)==\base_addr{LoopEntry}(p)&& \block_length{Here}(p)==\block_length{LoopEntry}(p)&& \valid {Here}(p)<==>\valid{LoopEntry}(p)&& \valid_read{Here}(p)<==>\valid_read{LoopEntry}(p)&& \allocation {Here}(p)==\allocation{LoopEntry}(p))Example 2.5112/*@ assert \forall integer j; 0<=j<n ==> \freeable(q[j]); *//*@ loop assignsq[0..(i-1)];63CHAPTER 2. SPECIFICATION LANGUAGE@ loop freesq[0..\at(i-1,LoopCurrent)];@ loop invariant \forall integer j ;0 <= j < i ==> \allocable(\at(q[j],LoopEntry));@ loop invariant \forall integer j ; 0 <= i <= n;@*/for (i=0; i<n; i++) {free(q[i]);q[i]=NULL;}3456789101112The addresses of locations q[0..n] are not modified by the loop, but their values are.

Theclause loop frees catches the set of the memory blocks that may have been released by theprevious loop iterations. The first loop invariant defines exactly these memory blocks. Onthe other hand, loop frees indicates that the remaining blocks have not been freed since thebeginning of the loop. Hence, they are still \freeable as expressed by the initial assert , andfree(q[i]) will succeed at next step.A loop-clause without an allocation clause implicitly states loop allocates \nothing .

Thatmeans the allocation status is not modified by the loop body. A loop-behavior withoutallocation clause means that the allocated and deallocated memory blocks are in fact specifiedby the allocation clauses of the loop-clauses (Grammar of loop-clauses and loop-behaviors isgiven in Figure 2.9).2.8Sets and lists2.8.1Finite setsSets of terms, as defined in Section 2.3.4, can be used as first-class values in annotations. Allthe elements of such a set must share the same type (modulo the usual implicit conversions).Sets have the built-in type set<A> where A is the type of terms contained in the set.In addition, it is possible to consider sets of pointers to values of different types. Inthis case, the set is of type set<char*> and each of its elements e is converted to(char*)e + (0..sizeof(*e)-1).Example 2.52 The following example defines the footprint of a structure, that is the set oflocations that can be accessed from an object of this type.1234struct S {char *x;int *y;};56//@ logic set<char*> footprint(struct S s) = \union(s.x,s.y) ;78910/*@ logic set<char*> footprint2(struct S s) =@\union(s.x,(char*)s.y+(0..sizeof(s.y)-1)) ;@*/111213/*@ axiomatic Conv {axiom conversion: \forall struct S s;642.8.

SETS AND LISTS141516*/}footprint(s) == \union(s.x,(char*) s.y + (0 .. sizeof(int) - 1));In the first definition, since the arguments of union are a set<char*> and a set<int*>, theresult is a set<char*> (according to typing of union). In other words, the two definitionsabove are equivalent.This logic function can be used as argument of \separated or assigns clause.Thus, the \separated predicate satisfies the following property (with s1 of type set<τ1 *> ands2 of type set<τ2 *>)123456\separated (s1 ,s2 ) <==>( \forall τ1 * p; \forall τ2 * q;\subset (p,s1 ) && \subset(q,s2 ) ==>( \forall \integer i,j;0 <= i < \sizeof(τ1 ) && 0 <= j < \sizeof(τ2 ) ==>(char*)p + i != (char*)q + j))and a clause assigns L1 ,. .

.,Ln is equivalent to the postcondition\forall char* p; \separated(\union(&L1 ,. . .,&Ln ),p) ==> *p == \old(*p)2.8.2Finite listsThe built-in type \list <A> can be used for finite sequences of elements of the same type A.For constructing such homogeneous lists, built-in functions and notations are available.The term \Nil denotes the empty sequence.\list <A> \Nil<A>;The function \Cons prepends an element elt onto a sequence tail\list <A> \Cons<A>(<A> elt, \list<A> tail);while \concat concatenates two sequences\list <A> \concat<A>( \list <A> front, \list<A> tail);and \repeat repeats a sequence n times, n being a positive number\list <A> \repeat<A>( \list <A> seq, integer n);The semantics of these functions rely on two useful functions: \length returns the number ofelements of a sequence seqinteger \length<A>( \list <A> seq);and \nth returns the element that is at position n of the given sequence seq.

The first elementis at position 0.<A> \nth<A>( \list <A> seq, integer n);Last but not least, the functions \repeat and \nth aren’t specified for negative number n. Thefunction \nth(l) is also unspecified for index greater than or equal to \length (l).The notation [| |] is just the same thing as \Nil and [|1,2,3|] is the sequence of threeintegers. In addition the infix operator ^ (resp. *^) is the same as function \concat (resp.\repeat ).65CHAPTER 2. SPECIFICATION LANGUAGEterm::=|||[| |][| term (, term)∗term ^ termterm*^ term|]empty listlist of elementslist concatenation (overloading bitwise-xoroperator)list repetitionFigure 2.22: Notations for built-in list datatypeExample 2.53 The following example illustrates the use of a such data structure and notations in connexion with ghost code.12345//@ ghost int ghost_trace;/*@ axiomatic TraceObserver {@logic \list < integer > observed_trace{L} reads ghost_trace;@ }@*/678910/*@ assigns ghost_trace;@ ensures register : observed_trace == (\old(observed_trace) ^ [| a |]);@*/void track(int a);1112131415161718192021222324252627282930313233343536373839/*@ requires empty_trace: observed_trace == \Nil;@ assigns ghost_trace;@ ensures head_seq: \nth(observed_trace,0) == x;@ behavior shortest_trace:@ assumes no_loop_entrance: n<=0;@ensures shortest_len: \length(observed_trace) == 2;@ensures shortest_seq: observed_trace == [| x, z |];@ behavior longest_trace:@ assumes loop_entrance: n>0;@ensures longest_len: \length(observed_trace) == 2+n;@ensures longest_seq:@observed_trace == ([| x |] ^ ([| y |] *^ n) ^ [| z |]);@*/void loops(int n, int x, int y, int z) {int i;//@ ghost track(x);/*@ loop assigns i, ghost_trace;@ loop invariant idx_min: 0<=i;@ loop invariant idx_max: 0<=n ? i<=n : i<=0;@ loop invariant inv_seq:@ observed_trace == (\at(observed_trace,LoopEntry) ^ ([| y |] *^ i));@*/for (i=0; i<n; i++) {//@ ghost track(y);;}//@ ghost track(z);}The function track adds a value to the tail of a ghost trace variable.

Calls to that functioninside ghost statements allow to modify that trace; and properties about the observed_tracecan be specified. Notice that the assigned ghost variable is ghost_trace.662.9. ABRUPT TERMINATIONabrupt-clause::=exits-clauseexits-clause::=exits predabrupt-clause-stmt::=breaks-clausebreaks-clause::=breaks predcontinues-clause::=continues predreturns-clause::=returns predterm::=\exit_status;| continues-clause|returns-clause;;;Figure 2.23: Grammar of contracts about abrupt terminations2.9Abrupt terminationThe ensures clause of function and statement contracts does not constrain the post-statewhen the annotated function and statement terminates respectively abruptly.

In such cases,abrupt clauses can be used inside simple clause or behavior body. The allowed constructsare shown in Figure 2.23.The clauses breaks , continues and returns can only be found in a statement contract andstate properties on the program state which hold when the annotated statement terminatesabruptly with the corresponding statement ( break , continue or return ).Inside these clauses, the construct \old(e) is allowed and denotes, like for statement contractsensures , assigns and allocates , the value of e in the pre-state of the statement.

Характеристики

Список файлов книги