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

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

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

(see [18]) and the tool ESC/Java2 for automaticdeductive verification of JML specifications (see [6]).One issue with such a desugaring approach is the complexity of the transformations involved,as e.g. for desugaring assignable clauses between multiple spec-cases in JML [22]. Anotherissue is precisely that tools only see one global contract, instead of multiple independentbehaviors, that could be analyzed separately in more detail. Instead, we favor the view thata function implements multiple behaviors, that can be analyzed separately if a tool feels likeit.

Therefore, we do not intend to provide a desugaring process.Axiomatized functions in specificationsJML only allows pure Java methods to be called in specifications [16]. This is certainlyunderstandable when relying on RAC: methods called should be defined so that the runtimecan call them, and they should not have side-effects in order not to pollute the program theyare supposed to annotate.91APPENDIX A. APPENDICESIn our setting, it is desirable to allow calls to logical functions in specifications. These functions may be defined, like program ones, but they may also be only declared (with a suitabledeclaration of reads clause) and defined through an axiomatization.

This makes for richerspecifications that may be useful either in automatic or in manual deductive verification.A.2.3Syntactic differencesThe following table summarizes the difference between JML keywords and ACSL ones, whenthe intent is the same, although minor differences might exist.A.3JMLmodifiable,assignablemeasured_byloop_invariantdecreasesACSLassignsdecreasesloop invariantloop variant( \forall τ x ; P ; Q)( \exists τ x ; P ; Q)\max τ x ; a <= x <= b ; f)( \forall τ x ; P ==> Q)( \exists τ x ; P && Q)\max(a,b,\lambda τ x ; f)Typing rulesDisclaimer: this section is unfinished, it is left here just to give an idea of what it will looklike in the final document.A.3.1Rules for termsInteger promotion:Γ`e:τΓ ` e : integerif τ is any C integer type char, short, int, or long, whatever attribute they have, inparticular signed or unsignedVariables:Γ ` id : τif id : τ ∈ ΓUnary integer operations:Γ ` t : integerif op ∈ {+, −, ∼}Γ ` op t : integerBoolean negation:Γ ` t : booleanΓ `! t : booleanPointer dereferencing:Γ ` t : τ∗Γ ` ∗t : τAddress operator:Γ`t:τΓ ` &t : τ ∗92A.4.

SPECIFICATION TEMPLATESBinaryΓ ` t1 : integerΓ ` t2 : integerif op ∈ {+, −, ∗, /, %}Γ ` t1 op t2 : integerΓ ` t1 : realΓ ` t2 : realif op ∈ {+, −, ∗, /}Γ ` t1 op t2 : realΓ ` t1 : integerΓ ` t2 : integerif op ∈ {==, ! =, <=, <, >=, >}Γ ` t1 op t2 : booleanΓ ` t1 : realΓ ` t2 : realif op ∈ {==, ! =, <=, <, >=, >}Γ ` t1 op t2 : booleanΓ ` t1 : τ ∗Γ ` t2 : τ ∗if op ∈ {==, ! =, <=, <, >=, >}Γ ` t1 op t2 : boolean(to be continued)A.3.2Typing rules for setsWe consider the typing judgement Γ, Λ ` s : τ, b meaning that s is a set of terms of type τ ,which is moreover a set of locations if the boolean b is true.

Γ is the C environment and Λis the logic environment.Rules:Γ, Λ ` id : τ, trueΓ, Λ ` id : τ, trueif id : τ ∈ Γif id : τ ∈ ΛΓ, Λ ` s : τ ∗, bΓ, Λ ` ∗s : τ, trueid : τ s : set < struct S∗ >` s− > id : set < τ >Γ, b ∪ Λ ` e : tsetτΓ, Λ ` {e | b; P } : tsetτΓ, Λ ` e1 : τ, b Γ, Λ ` e2 : τ, bΓ, Λ ` e1 , e2 : τ, bA.4Specification TemplatesThis section describes some common issues that may occur when writing an ACSL specification and proposes some solution to overcome themA.4.1Accessing a C variable that is maskedThe situation may happen where it is necessary to refer in an annotation to a C variablethat is masked at that point. For instance, a function contract may need to refer to a globalvariable that has the same name as a function parameter, as in the following code:93APPENDIX A. APPENDICES123int x;//@ assigns x;int g();45678int f(int x) {// ...return g();}In order to write the assigns clause for f, we must access the global variable x, since f callsg, which can modify x.

This is not possible with C scoping rules, as x refers to the parameterof f in the scope of the function.A solution is to use a ghost pointer to x, as shown in the following code:1int x;23//@ ghost int* const ghost_ptr_x = &x;456//@ assigns x;int g();789101112A.5//@ assigns *ghost_ptr_x;int f(int x) {// ...return g();}Illustrative exampleThis is an attempt to define an example for ACSL, much as the Purse example in JMLdescription papers. It is a memory allocator, whose main functions are memory_alloc andmemory_free, to respectively allocate and deallocate memory.

The goal is to exercise as muchas possible of ACSL.12#include <stdlib.h>34#define DEFAULT_BLOCK_SIZE 100056typedef enum _bool { false = 0, true = 1 } bool;7891011121314151617181920/*@ predicate finite_list<A>((A* -> A*) next_elem, A* ptr) =@ ptr == \null ||@ ( \valid (ptr) && finite_list(next_elem,next_elem(ptr))) ;@@ logic integer list_length<A>((A* -> A*) next_elem, A* ptr) =@ (ptr == \null) ? 0 :@ 1 + list_length(next_elem,next_elem(ptr)) ;@@@ predicate lower_length<A>((A* -> A*) next_elem,@A* ptr1, A* ptr2) =@ finite_list(next_elem, ptr1) && finite_list(next_elem, ptr2)@ && list_length(next_elem, ptr1) < list_length(next_elem, ptr2) ;94A.5. ILLUSTRATIVE EXAMPLE21@*/222324// forward referencestruct _memory_slice;25262728293031323334353637383940414243444546/* A memory block holds a pointer to a raw block of memory allocated by* calling [malloc].

It is sliced into chunks, which are maintained by* the [slice] structure. It maintains additional information such as* the [size] of the memory block, the number of bytes [used] and the [next]* index at which to put a chunk.*/typedef struct _memory_block {//@ ghost booleanpacked;// ghost field [packed] is meant to be used as a guard that tells when// the invariant of a structure of type [memory_block] holdsunsigned intsize;// size of the array [data]unsigned intnext;// next index in [data] at which to put a chunkunsigned intused;// how many bytes are used in [data], not necessarily contiguous oneschar*data;// raw memory block allocated by [malloc]struct _memory_slice* slice;// structure that describes the slicing of a block into chunks} memory_block;47484950515253545556/*@ strong type invariant inv_memory_block(memory_block mb) =@ mb.packed ==>@(0 < mb.size && mb.used <= mb.next <= mb.size@&& \offset (mb.data) == 0@&& \block_length(mb.data) == mb.size) ;@@ predicate valid_memory_block(memory_block* mb) =@\valid (mb) && mb->packed ;@*/5758596061626364656667686970717273747576/* A memory chunk holds a pointer [data] to some part of a memory block* [block].

It maintains the [offset] at which it points in the block, as well* as the [size] of the block it is allowed to access. A field [free] tells* whether the chunk is used or not.*/typedef struct _memory_chunk {//@ ghost boolean packed;// ghost field [packed] is meant to be used as a guard that tells when// the invariant of a structure of type [memory_chunk] holdsunsigned intoffset;// offset at which [data] points into [block->data]unsigned intsize;// size of the chunkboolfree;// true if the chunk is not used, false otherwisememory_block* block;// block of memory into which the chunk pointschar*data;// shortcut for [block->data + offset]95APPENDIX A.

APPENDICES77} memory_chunk;787980818283848586878889909192/*@ strong type invariant inv_memory_chunk(memory_chunk mc) =@ mc.packed ==>@(0 < mc.size && valid_memory_block(mc.block)@&& mc.offset + mc.size <= mc.block->next) ;@@ predicate valid_memory_chunk(memory_chunk* mc, int s) =@\valid (mc) && mc->packed && mc->size == s ;@@ predicate used_memory_chunk(memory_chunk mc) =@ mc.free == false ;@@ predicate freed_memory_chunk(memory_chunk mc) =@ mc.free == true ;@*/93949596979899100101102103104/* A memory chunk list links memory chunks in the same memory block.* Newly allocated chunks are put first, so that the offset of chunks* decreases when following the [next] pointer.

Allocated chunks should* fill the memory block up to its own [next] index.*/typedef struct _memory_chunk_list {memory_chunk*chunk;// current list elementstruct _memory_chunk_list* next;// tail of the list} memory_chunk_list;105106107108109110111112113114115116117118119120121122123124125126127128129130131132/*@ logic memory_chunk_list* next_chunk(memory_chunk_list* ptr) =@ ptr->next ;@@ predicate valid_memory_chunk_list@(memory_chunk_list* mcl, memory_block* mb) =@\valid (mcl) && valid_memory_chunk(mcl->chunk,mcl->chunk->size)@ && mcl->chunk->block == mb@ && (mcl->next == \null ||@valid_memory_chunk_list(mcl->next, mb))@ && mcl->offset == mcl->chunk->offset@ && (@// it is the last chunk in the list@(mcl->next == \null && mcl->chunk->offset == 0)@||@// it is a chunk in the middle of the list@(mcl->next != \null@&& mcl->next->chunk->offset + mcl->next->chunk->size@== mcl->chunk->offset)@)@ && finite_list(next_chunk, mcl) ;@@ predicate valid_complete_chunk_list@(memory_chunk_list* mcl, memory_block* mb) =@ valid_memory_chunk_list(mcl,mb)@ && mcl->next->chunk->offset +@mcl->next->chunk->size == mb->next ;@96A.5.

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

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