ACSL Language Reference (811287), страница 5
Текст из файла (страница 5)
Section 2.2.7 details the use of arrays as logic values. There are also differencesbetween t and the pointer to its first element when evaluating an expression at a givenprogram point. See Section 2.4.3 for more information.Function pointersPointers to C functions are allowed in logic. The only possible use of them is to check forequality.Example 2.11int f(int x);int g(int x);//@ requires p == &f || p == &g;void h(int(*p)(int)) {...}2.2.7Structures, Unions and Arrays in logicAggregate C objects (i.e. structures, unions and arrays) are also possible values for terms inlogic.
They can be passed as parameters (and also returned) to logic functions, tested forequality, etc. like any other values.Aggregate types can be declared in logic, and their contents may be any logic types themselves. Constructing such values in logic can be performed using a syntax similar to Cdesignated initializers.Example 2.12 Array types in logic may be declared either with or without an explicit nonnegative length. Access to the length of a logic array can be done with \length .262.2.
LOGIC EXPRESSIONS//@ type point = struct { real x; real y; };//@ type triangle = point[3];//@ logic point origin = { .x = 0.0 , .y = 0.0 };/*@ logic triangle t_iso = { [0] = origin,@[1] = { .y = 2.0 , .x = 0.0 }@[2] = { .x = 2.0 , .y = 0.0 }};@*//*@ logic point centroid(triangle t) = {@.x = mean3(t[0].x,t[1].x,t[2].x);@.y = mean3(t[0].y,t[1].y,t[2].y);@ };@*///@ type polygon = point[];/*@ logic perimeter(polygon p) =@ \sum(0,\length(p)-1,\lambda integer i;d(p[i],p[(i+1) % \length(p)])) ;@*/Beware that because of the principle of only total functions in logic, t[i] can appear in ACSLannotations even if i is outside the array bounds.Functional updatesSyntax for functional update is similar to initialization of aggregate objects.Example 2.13 Functional update of an array is done by{ t_iso \with [0] = { .x = 3.0, .y = 3.0 } }Functional update of a structure is done by{ origin \with .x = 3.0 }There is no particular syntax for functional update of a union.
For an object of an uniontype, the following equality is not true{ { object \with .x = 3.0 }\with .y = 2.0 } == { { object \with .y = 2.0 }\with .x = 3.0 }The equality predicate == applies to aggregate values, but it is required that they have thesame type.
Then equality amounts to recursively checking equality of fields. Equality ofarrays of different lengths returns false. Beware that equality of unions is also equality of allfields.C aggregate typesC aggregate types (struct, union or array) naturally map to logic types, by recursively mapping their fields.Example 2.14 There is no implicit cast to type of the updated/initialized fields.27CHAPTER 2. SPECIFICATION LANGUAGEstruct S { int x; float y; int t[10]; };//@ logic integer f( struct S s) = s.t[3];//@ logic struct S g(integer n, struct S s) = { s \with .x = (int)n };Unlike in C, all fields should be initialized:/*@ logic struct S h(integer n, int a[10]) = {@ .x = (int)n, .y = (float)0.0, .t = a@ };@*/Cast and conversionUnlike in C, there is no implicit conversion from an array type to a pointer type. On theother hand, there is an implicit conversion from an array of a given size to an array withunspecified size (but not the converse).Example 2.15//@ logic point square[4] = { origin, ...
};//@ ... perimeter(square);// well-typed//@ ... centroid(square);// wrongly typed//@ ... centroid((triangle)square); // well-typed (truncation)An explicit cast from an array type to a pointer type is allowed only for arrays that lie in Cmemory. As in C, the result of the cast is the address of the first element of the array (seeSection 2.2.6).Conversely, an explicit cast from a pointer type to an array type acts as collecting the valuesit points to.Subtyping and cast recursively applies to fields.Example 2.16struct { float u,v; } p[10];//@ assert centroid((point[3])p) == ...//@ assert perimeter((point[])p) == ...Precisely, conversion of a pointer p of type τ ∗ to an logic array of type τ [] returns a logicarray t such thatlength(t) = (\block_length(p) − \offset (p))/ sizeof (τ )More generaly, an explicit cast from a C aggregate of type τ to another C aggregate typeis allowed for being able to specify such a value conversion into logical functions or functioncontracts without using the addressing operator &.Example 2.17 Unlike in C, conversion of an aggregate of C type struct τ to another structure type is allowed.282.3.
FUNCTION CONTRACTSa::=requires-clause ∗ terminates-clause ?decreases-clause ? simple-clause ∗named-behavior ∗ completeness-clause ∗requires-clause::=requiresterminates-clause::=terminates preddecreases-clause::=decreases termsimple-clause::=|assigns-clause | ensures-clauseallocation-clause | abrupt-clauseassigns-clause::=assigns locationslocations::=locationlocation::=tsetensures-clause::=ensures prednamed-behavior::=behavior idbehavior-body::=assumes-clause ∗assumes-clause::=assumes predcompleteness-clause::=|complete behaviors (iddisjoint behaviors (idfunction-contracta;pred;;( for id)?;(, location)∗|\nothing;: behavior-bodyrequires-clause ∗simple-clause ∗;(, id)∗ )?(, id)∗ )?;;empty contracts are forbiddenFigure 2.5: Grammar of function contractsterm::=|\old ( term\result)pred::=\old ( pred)old valueresult of a functionFigure 2.6: \old and \result in termsstruct long_st { int x1,y2;};struct st { char x,y; };//@ ensures \result == (struct st) s;struct st from_long_st(struct long_st s) {return *( struct st *)&s;}2.3Function contractsFigure 2.5 shows a grammar for function contracts.
Location denotes a memory locationand is defined in Section 2.3.4. Allocation-clauses allow to specify which memory location isdynamically allocated or deallocated by the function from the heap; they are defined later inSection 2.7.3.This section is organized as follows. First, the grammar for terms is extended with two new29CHAPTER 2. SPECIFICATION LANGUAGEconstructs. Then Section 2.3.2 introduces simple contracts. Finally, Section 2.3.3 definesmore general contracts involving named behaviors.The decreases and terminates clauses are presented later in Section 2.5.
Abrupt-clauses allowto specify what happens when the function does not return normally but exits abruptly;they are defined in Section 2.9.2.3.1Built-in constructs \old and \resultPost-conditions usually require to refer to both the function result and values in the pre-state.Thus terms are extended with the following new constructs (shown in Figure 2.6).• \old(e) denotes the value of predicate or term e in the pre-state of the function.• \result denotes the returned value of the function.\old(e) and \result can be used only in ensures clauses, since the other clauses already referto the pre-state.
In addition, \result can not be used in the contract of a function whichreturns void .C function parameters are obtained by value from actual parameters that mostly remainunaltered by the function calls. For that reason, formal parameters in function contractsare defined such that they always refer implicitly to their values interpreted in the pre-state.Thus, the \old construct is useless for formal parameters (in function contracts only).2.3.2Simple function contractsA simple function contract, having only simple clauses and no named behavior, takes thefollowing form:1234/*@ requires P1 ; requires P2 ; ...@ assigns L1 ; assigns L2 ; ...@ ensures E1 ; ensures E2 ; ...@*/The semantics of such a contract is as follows:• The caller of the function must guarantee that it is called in a state where the propertyP1 && P2 && ...
holds.• The called function returns a state where the property E1 && E2 && ... holds.• All memory locations that are allocated in both the pre-state and the post-state1 anddo not belong to the set L1 ∪ L2 ∪ . . . are left unchanged in the post-state. The setL1 ∪ L2 ∪ . .
. itself is interpreted in the pre-state.Having multiple requires , assigns , or ensures clauses only improves readability since the contract above is equivalent to the following simplified one:12341/*@ requires P1 && P2 && ...;@ assigns L1 , L2 ,...;@ ensures E1 && E2 && ...;@*/Functions that allocate or free memory can be specified with additional clauses described in section 2.7.3.302.3.
FUNCTION CONTRACTSIf no clause requires is given, it defaults to \true , and similarly for ensures clause. Giving noassigns clause means that locations assigned by the function are not specified, so the callerhas no information at all on this function’s side effects. See Section 2.3.5 for more details ondefault status of clauses.Example 2.18 The following function is given a simple contract for computation of theinteger square root.123456/*@ requires x >= 0;@ ensures \result >= 0;@ ensures \result * \result <= x;@ ensures x < ( \result + 1) * (\result + 1);@*/int isqrt(int x);The contract means that the function must be called with a nonnegative argument, and returnsa value satisfying the conjunction of the three ensures clauses. Inside these ensures clauses,the use of the construct \old(x) is not necessary, even if the function modifies the formalparameter x, because function calls modify a copy of the effective parameters, and the effectiveparameters remain unaltered.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
