ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver (1185160), страница 3
Текст из файла (страница 3)
The grammar for binders andtype expressions is given separately in Figure 2.3.With respect to C pure expressions, the additional constructs are as follows:162.2. LOGIC EXPRESSIONSAdditional connectives C operators && (UTF8: ∧), || (UTF8: ∨) and ! (UTF8: ¬) areused as logical connectives. There are additional connectives ==> (UTF8: =⇒) forimplication, <==> (UTF8: ⇐⇒) for equivalence and ^^ (UTF8: ⊕) for exclusive or.These logical connectives all have a bitwise counterpart, either C ones like &, |, ~ and^, or additional ones like bitwise implication --> and bitwise equivalence <-->.Quantification Universal quantification is denoted by \forall τ x1 ,.
. .,xn ; e and existential quantification by \exists τ x1 ,. . .,xn ; e.Local binding \let x = e1 ;e2 introduces the name x for expression e1 which can be used inexpression e2 .Conditional c ? e1 : e2 . There is a subtlety here: the condition may be either a booleanterm or a predicate.
In case of a predicate, the two branches must be also predicates,so that this construct acts as a connective with the following semantics: c ? e1 : e2 isequivalent to (c ==> e1 ) && (! c ==> e2 ).Syntactic naming id : e is a term or a predicate equivalent to e.
It is different from localnaming with \let : the name cannot be reused in other terms or predicates. It is onlyfor readibility purposes.Functional modifier The composite element modifier is an additional operator related toC structure field and array accessors. The expression { s \with .id = v } denotes thesame structure as s, except for the field id that is equal to v. The equivalent expressionfor an array is { t \with [ i ] = v } which returns the same array as t, except for theith element whose value is v. See section 2.10 for an example of use of these operators.rel-op::=== |!= |<= |>= |> |pred::=|||||||||||||||||\true | \falseterm (rel-op term)+id ( term (, term)∗ )( pred )pred && predpred || predpred ==> predpred <==> pred! predpred ^^ predterm ? pred : predpred ? pred : pred\let id = term ; pred\let id = pred ; pred\forall binders ; pred\exists binders ; predid : predstring : pred<comparisons (see remark)predicate applicationparenthesesconjunctiondisjunctionimplicationequivalencenegationexclusive orternary conditionlocal bindinguniversal quantificationexistential quantificationsyntactic namingsyntactic namingFigure 2.2: Grammar of predicates17CHAPTER 2.
SPECIFICATION LANGUAGE(, binder)∗binders::=binderbinder::=type-expr variable-ident(,variable-ident)∗type-expr::=logic-type-exprlogic-type-expr::=|built-in-logic-typeidbuilt-in-logic-type::=boolean |variable-ident::=||id | * variable-identvariable-ident []( variable-ident )| C-type-nameinteger |type identifierrealFigure 2.3: Grammar of binders and type expressionsLogic functions Applications in terms and in propositions are not applications of C functions, but of logic functions or predicates; see Section 2.6 for detail.Consecutive comparison operators Theconstructt1 relop1 t2 relop2 t3 · · · tkwithseveralconsecutivecomparisonoperatorsisashortcutfor(t1 relop1 t2 ) && (t2 relop2 t3 ) && · · ·.It is required that the relopi operatorsmust be in the same “direction”, i.e.
they must all belong either to {<, <=, ==} or to{>,>=,==}. Expressions such as x < y > z or x != y != z are not allowed.To enforce the same interpretation as in C expressions, one may need to add extra parentheses: a == b < c is equivalent to a == b && b < c, whereas a == (b < c) is equivalentto \let x = b < c; a == x. This situation raises some issues, as in the example below.There is a subtlety regarding comparison operators: they are predicates when used in predicate position, and boolean functions when used in term position.Example 2.1 Let us consider the following example:int f(int a, int b) { return a < b; }• the obvious postcondition \result == a < b is not the right one because it is actually ashortcut for \result == a && a < b.• adding parentheses results in a correct post-condition \result == (a < b).
Note howeverthat there is an implicit conversion (see Sec. 2.2.3) from the int (the type of \result )to boolean (the type of (a<b))• an equivalent post-condition, which does not rely on implicit conversion, is( \result != 0) == (a<b). Both pairs of parentheses are mandatory.• \result == (integer)(a<b) is also acceptable because it compares two integers. The casttowards integer enforces a<b to be understood as a boolean term. Notice that a casttowards int would also be acceptable.• \result != 0 <==> a < b is acceptable because it is an equivalence between two predicates.182.2. LOGIC EXPRESSIONSclassselectionunarymultiplicativeadditiveshiftcomparisoncomparisonbitwise andbitwise xorbitwise orbitwise impliesbitwise equivconnective andconnective xorconnective orconnective impliesconnective equivternary connectivebindingnamingassociativityleftrightleftleftleftleftleftleftleftleftleftleftleftleftleftrightleftrightleftrightoperators[· · ·] -> .! ~ + - * & (cast) sizeof*/%+<< >>< <= > >=== !=&^|--><-->&&^^||==><==>· · ·?· · ·:· · ·\forall \exists \let:Figure 2.4: Operator precedence2.2.1Operators precedenceThe precedence of C operators is conservatively extended with additional operators, as shownin Figure 2.4.
In this table, operators are sorted from highest to lowest priority. Operatorsof same priority are presented on the same line.There is a remaining ambiguity between the connective · · ·?· · ·:· · · and the labelling operator :.Consider for instance the expression x?y:z:t. The precedence table does not indicate whetherthis should be understood as x?(y:z):t or x?y:(z:t).
Such a case must be considered as asyntax error, and should be fixed by explicitly adding parentheses.2.2.2SemanticsThe semantics of logic expressions in ACSL is based on mathematical first-order logic [25]. Inparticular, it is a 2-valued logic with only total functions. Consequently, expressions are never“undefined”. This is an important design choice and the specification writer should be aware ofthat. (For a discussion about the issues raised by such design choices, in similar specificationlanguages such as JML, see the comprehensive list compiled by Patrice Chalin [4, 5].)Having only total functions implies than one can write terms such as 1/0, or *p when p is null(or more generally when it points to a non-properly allocated memory cell).
In particular,the predicates1/0*p====1/0*pare valid, since they are instances of the axiom ∀x, x = xof first-order logic. The reader should not be alarmed, because there is no way to deduceanything useful from such terms. As usual, it is up to the specification designer to writeconsistent assertions. For example, when introducing the following lemma (see Section 2.6):19CHAPTER 2. SPECIFICATION LANGUAGE123/*@ lemma div_mul_identity:@\forall real x, real y; y != 0.0 ==> y*(x/y) == x;@*/a premise is added to require y to be non zero.2.2.3TypingThe language of logic expressions is typed (as in multi-sorted first-order logic). Types areeither C types or logic types defined as follows:• “mathematical” types: integer for unbounded, mathematical integers, real for realnumbers, boolean for booleans (with values written \true and \false );• logic types introduced by the specification writer (see Section 2.6).There are implicit coercions for numeric types:• C integral types char , short , int and long , signed or unsigned, are all subtypes of typeinteger ;• integer is itself a subtype of type real ;• C types float and double are subtypes of type real .Notes:• There is a distinction between booleans and predicates.
The expression x<y in termposition is a boolean, and the same expression is also allowed in predicate position.• Unlike in C, there is a distinction between booleans and integers. There is an implicit promotion from integers to booleans, thus one may write x && y instead ofx != 0 && y != 0. If the reverse conversion is needed, an explicit cast is required,e.g. ( int )(x>0)+1, where \false becomes 0 and \true becomes 1.• Quantification can be made over any type: logic types and C types.
Quantificationover pointers must be used carefully, since it depends on the memory state wheredereferencing is done (see Section 2.2.4 and Section 2.6.9).Formal typing rules for terms are given in appendix A.3.2.2.4Integer arithmetic and machine integersThe following integer arithmetic operations apply to mathematical integers: addition, subtraction, multiplication, unary minus. The value of a C variable of an integral type is promoted to a mathematical integer. As a consequence, there is no “arithmetic overflow” in logicexpressions.Division and modulo are also mathematical operations, which coincide with the correspondingC operations on C machine integers, thus following the ISO C99 conventions.
In particular,these are not the usual mathematical Euclidean division and remainder. Generally speaking,division rounds the result towards zero. The results are not specified if divisor is zero;otherwise if q and r are the quotient and the remainder of n divided by d then:202.2.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
