ACSL Language Reference (811287), страница 14
Текст из файла (страница 14)
They are not lvalues, thus theycannot be assigned directly (unlike ghost variables, see below).• Nevertheless, a function contract might state that a model variable is assigned.• When a function contract mentions model variables:– the precondition is implicitly existentially quantified over those variables;– the postconditions are universally quantified over the old values of model variables,and existentially quantified over the new values.Thus, in practice, the only way to prove that a function body satisfies a contract with modelvariables is to provide an invariant relating model variables and concrete variables, as in theexample below.Model fields behave the same, but they are attached to any value whose static type is the oneof the model declaration.
A model field can be attached to any C type, not only to struct.When it is attached to a compound type, however, it must not have the same name as a Cfield of the corresponding type. In addition, model fields are “inherited” by a typedef in thesense that the newly defined type has also the model fields of its parents (and can acquiremore, which will not be present for the parent). For instance, in the following code, t1 hasone model field m1, while t2 has two model fields, m1 and m2.1234typedef int t1;typedef t1 t2;/*@ model t1 { int m1 }; *//*@ model t2 { int m2 }; */declaration::=||C-declaration/*@ model parameter ; *//*@ model C-type-name { parameter;?} ;model variablemodel field*/Figure 2.26: Grammar for declarations of model variables and fields73CHAPTER 2.
SPECIFICATION LANGUAGEExample 2.61 Here is an example of a specification for a function which generates freshintegers. The contract is given in term of a model variable which is intended to represent theset of “forbidden” values, e.g. the values that have already been generated.1/* public interface */23//@ model set<integer> forbidden = \empty;456789/*@ assigns forbidden;@ ensures ! \subset( \result ,\old(forbidden))@ && \subset( \result ,forbidden) && \subset(\old(forbidden),forbidden);@*/int gen();The contract is expressed abstractly, telling that• the forbidden set of values is modified;• the value returned is not in the set of forbidden values, thus it is “fresh”;• the new set of forbidden values contains both the value returned and the previous forbidden values.
The new set may have more values than the union of { \result } and\old(forbidden).An implementation of this function might be as follows, where a decision has been made togenerate values in increasing order, so that it is sufficient to record the last value generated.This decision is made explicit by an invariant.12345678/* implementation */int gen() {static int x = 0;/*@ global invariant I: \forall integer k;@Set::mem(k,forbidden) ==> x > k;@*/return x++;}Remarks Although the syntax of model variables is close to JML model variables, theydiffer in the sense that the type of a model variable is a logic type, not a C type. Also, thesemantics above is closer to the one of B machines [1].
It has to be noticed that programverification with model variables does not have a well-established theoretical background [19,17], so we deliberately do not provide a precise semantics in this document .2.12Ghost variables and statementsGhost variables and statements are like C variables and statements, but visible only in thespecifications. They are introduced by the ghost keyword at the beginning of the annotation(i.e. /*@ ghost ... */ or //@ ghost ... for a one-line ghost code, as mentioned in section 1.2).The grammar is given in Figure 2.27, in which only the first form of annotation is used.In this figure, the C-* non-terminals refer to the corresponding grammar rules of the ISOstandard, without any ACSL extension. Any non terminal of the form ghost-non-term for742.12.
GHOST VARIABLES AND STATEMENTSwhich no definition is given in the figure represents the corresponding C-non-term entry, inwhich any entry is substituted by ghost-entry.The variations with respect to the C grammar are the following:• Comments must be introduced by // and extend until the end of the line (the ghostcode itself is placed inside a C comment.
/* ... */ would thus lead to incorrect Ccode).• It is however possible to write multi-line annotations inside ghost code. These annotations are enclosed between /@ and @/ (since as indicated above, /*@ ... */ would leadto incorrect C code). As in normal annotations, @ characters at the beginning of a lineand at the end of an annotation (before the final @/) are considered as blank.• Logical types, such as integer or real are authorized in ghost code.• A non-ghost function can take ghost parameters.
If such a ghost clause is present in thedeclarator, then the list of ghost parameters must be non-empty and fixed (no varargghost). The call to the function must then provide the appropriate number of ghostparameters.• Any non-ghost if-statement which does not have a non-ghost else clause can be augmented with a ghost one. Similarly, a non-ghost switch can have a ghost default : clauseif it does not have a non-ghost one (there are however semantic restrictions for validghost labelled statements in a switch, see next paragraph for details).Semantics of Ghost Code The question of semantics is essential for ghost code.
Informally, the semantics requires that ghost statements do not change the regular programexecution. This implies several conditions, including e.g.:• Ghost code cannot modify a non-ghost C variable.• Ghost code cannot modify a non-ghost structure field.• If p is a ghost pointer pointing to a non-ghost memory location, then it is forbidden toassign *p.• The body of a ghost function is ghost code, and hence may not modify non-ghostvariables or fields.• If a non-ghost C function is called in ghost code, it must not modify non-ghost variablesor fields.• If a structure has ghost fields, the sizeof of the structure is the same has the structurewithout ghost fields.
Also, alignment of fields remains unchanged.• The control-flow graph of a function must not be altered by ghost statements. Inparticular, no ghost return can appear in the body of a non-ghost function. Similarly,ghost goto, break , and continue continue cannot jump outside of the innermost non-ghostenclosing block.75CHAPTER 2. SPECIFICATION LANGUAGEghost-type-specifier::=|C-type-specifierlogic-typedeclaration::=|C-declaration/*@ ghostghost-declarationdirect-declarator::=|*/C-direct-declaratordirect-declarator( C-parameter-type-list?)/*@ ghost( ghost-parameter-type-list )*/postfix-expression::=|C-postfix-expressionpostfix-expression( C-argument-expression-list?)/*@ ghost( ghost-argument-expression-list )*/statement::=|C-statementstatements-ghoststatements-ghost::=/*@ ghostghost-statement+ghost-selection-statement::=|ghost argscall with ghosts*/C-selection-statementif ( C-expression )statement/*@ ghost elseghost-statement+*/struct-declaration::=|C-struct-declaration/*@ ghoststruct-declaration*/ghost fieldFigure 2.27: Grammar for ghost statementsSemantics is specified as follows.
First, the execution of a program with ghost code involvesa ghost memory heap and a ghost stack, disjoint from the regular heap and stack. Ghostvariables lie in the ghost heap, as do the ghost fields of structures. Thus, every memory sideeffect can be classified as ghost or non-ghost. Then, the semantics is that memory side-effectsof ghost code must always be in the ghost heap or the ghost stack.Notice that this semantics is not statically decidable. It is left to tools to provide approximations, correct in the sense that any code statically detected as ghost must be semanticallyghost.Example 2.62 The following example shows some invalid assignments of ghost pointers:12void f(int x, int *q) {762.12.
GHOST VARIABLES AND STATEMENTS//@ ghost int *p = q;//@ ghost *p = 0;// above assignment is wrong: it modifies *q which lies// in regular memory heap34567//@ ghost p = &x;//@ ghost *p = 0;// above assignment is wrong: it modifies x which lies// in regular memory stack8910111213}Example 2.63 The following example shows some invalid ghost statements:123456789101112int f (int x, int y) {//@ ghost int z = x + y;switch (x) {case 0: return y;//@ ghost case 1: z=y;// above statement is correct.//@ ghost case 2: { z++; break; }// invalid, would bypass the non-ghost defaultdefault : y++;}return y;}1314151617181920int g(int x) {//@ ghost int z = x;if (x > 0) { return x; }//@ ghost else { z++; return x; }// invalid, would bypass the non-ghost returnreturn x+1;}Differences between model variables and ghost variables A ghost variable is anadditional specification variable which is assigned in ghost code like any C variable.
On theother hand, a model variable cannot be assigned, but one can state it is modified and canexpress properties about the new value, in a non-deterministic way, using logic assertions andinvariants. In other words, specifications using ghost variable assignments are executable.Example 2.64 The example 2.61 can also be specified with a ghost variable instead of amodel variable:1//@ ghost set<integer> forbidden = \empty;2345678910/*@ assigns forbidden;@ ensures ! \subset( \result ,\old(forbidden))@ && \subset( \result ,forbidden)&& \subset(\old(forbidden),forbidden);@*/int gen() {static int x = 0;/*@ global invariant I: \forall integer k;77CHAPTER 2. SPECIFICATION LANGUAGE111213141516}2.12.1@\subset (k,forbidden) ==> x > k;@*/x++;//@ ghost forbidden = \union(x,forbidden);return x;Volatile variablesVolatile variables can not be used in logic terms, since reading such a variable may have aside effect, in particular two successive reads may return different values.declaration::=//@volatilelocations( reads id)?(writes id)?;Figure 2.28: Grammar for volatile constructsSpecifying properties of a volatile variable may be done via a specific construct to attachtwo ghost functions to it.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
