Authors Julien Signoles
License CC-BY-SA-4.0
E-ACSL Executable ANSI/ISO C Specification Language Version 1.19 Julien Signoles Work licensed under Creative Commons BY-SA licence https://creativecommons.org/licenses/by-sa/4.0/ © 2011-2023 CEA LIST Contents 1 Introduction 5 1.1 Organization of this document . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.2 Generalities about Annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.3 Notations for grammars . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2 Specification language 6 2.1 Lexical rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.2 Logic expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.2.1 Operators precedence . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.2.3 Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.2.4 Integer arithmetic and machine integers . . . . . . . . . . . . . . . . . 12 2.2.5 Real numbers and floating point numbers . . . . . . . . . . . . . . . . 12 2.2.6 C arrays and pointers . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.2.7 Structures, Unions and Arrays in logic . . . . . . . . . . . . . . . . . . 12 2.3 Function contracts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.3.1 Built-in constructs \old and \result . . . . . . . . . . . . . . . . . . 12 2.3.2 Simple function contracts . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.3.3 Contracts with named behaviors . . . . . . . . . . . . . . . . . . . . . . 12 2.3.4 Memory locations and sets of terms . . . . . . . . . . . . . . . . . . . . 14 2.3.5 Default contracts, multiple contracts . . . . . . . . . . . . . . . . . . . 14 2.4 Statement annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.4.1 Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.4.2 Loop annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.4.3 Built-in construct \at . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.4.4 Statement contracts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.5 Termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.5.1 Integer measures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.5.2 General measures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.5.3 Recursive function calls . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.5.4 Non-terminating functions . . . . . . . . . . . . . . . . . . . . . . . . . 19 2 CONTENTS 2.6 Logic specifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.6.1 Predicate and function definitions . . . . . . . . . . . . . . . . . . . . . 19 2.6.2 Lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.6.3 Inductive predicates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.6.4 Axiomatic definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.6.5 Polymorphic logic types . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.6.6 Recursive logic definitions . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.6.7 Higher-order logic constructions . . . . . . . . . . . . . . . . . . . . . . 22 2.6.8 Concrete logic types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.6.9 Hybrid functions and predicates . . . . . . . . . . . . . . . . . . . . . . 22 2.6.10 Memory footprint specification: reads clause . . . . . . . . . . . . . . 22 2.6.11 Specification Modules . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.7 Pointers and physical adressing . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 2.7.1 Memory blocks and pointer dereferencing . . . . . . . . . . . . . . . . . 24 2.7.2 Separation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.7.3 Dynamic allocation and deallocation . . . . . . . . . . . . . . . . . . . 25 2.8 Sets and lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.8.1 Finite sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.8.2 Finite lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.9 Abrupt termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.10 Dependencies information . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.11 Data invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.11.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.11.2 Model variables and model fields . . . . . . . . . . . . . . . . . . . . . 26 2.12 Ghost variables and statements . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.12.1 Volatile variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.13 Initialization and undefined values . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.14 Dangling pointers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.15 Well-typed pointers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.16 Logic attribute annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.17 Preprocessing for ACSL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3 Libraries 30 4 Conclusion 31 A Appendices 32 A.1 Changes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Bibliography 35 List of Figures 36 Index 37 3 Foreword This document describes version 1.19 of the E-ACSL specification language. It is based on the ACSL specification language [2]. Features of both languages may still evolve in the future, even if we do our best to preserve backward compatibility. In particular, some features are considered experimental, meaning that their syntax and semantics is not yet fixed. These features are marked with Experimental. Acknowledgements We gratefully thank all the people who contributed to this document: Patrick Baudin, Bernard Botella, Thibaut Benjamin, Loïc Correnson, Pascal Cuoq, Basile Desloges, Johannes Kanig, André Maroneze, Fonenantsoa Maurica, David Mentré, Benjamin Monate, Yannick Moy and Virgile Prevosto. This work has been initially supported by the ‘Hi-Lite’ FUI project (FUI AAP 9). 4 Introduction 1 This document is a reference manual for E-ACSL. E-ACSL is an acronym for “Executable ANSI/ISO C Specification Language”. It is an “executable” subset of ACSL [2] implemented [3] in the Frama-C platform [7]. Contrary to ACSL, each E-ACSL specification is executable: it may be evaluated at runtime. In this document, we assume that the reader has a good knowledge of both ACSL [2] and the ANSI C programming language [8, 9]. 1.1 Organization of this document This document is organized in the very same way that the reference manual of ACSL [2]. Instead of being a fully new reference manual, this document points out the differences between E-ACSL and ACSL. Each E-ACSL construct which is not pointed out must be considered to have the very same semantics than its ACSL counterpart. For clarity, each relevant grammar rules are given in BNF form in separate figures like the ACSL reference manual does. In these rules, constructs with semantic changes are displayed in blue. 1.2 Generalities about Annotations No difference with ACSL. 1.3 Notations for grammars No difference with ACSL. 5 Specification language 2 2.1 Lexical rules No difference with ACSL. 2.2 Logic expressions No difference with ACSL, but the quantifications must be guarded. More precisely, the grammars of terms and binders presented respectively Figures 2.1 and 2.3 are the same than the ones of ACSL, while Figure 2.2 presents the grammar of predicates. The only differences introduced by E-ACSL with respect to ACSL are the fact that the quantifications that must be guarded and the introduction of iterators. Quantification The general form of quantifications (called generalized quantifications below), as described in Fig. 2.2, is restricted to a few finite enumerable types: the types of bound variables must be C integer types, enum types, pointer types, or their aliases. Generalized quantification over large types (for instance, types containing 232 elements). are unlikely evaluated efficiently at runtime. In addition to generalized quantifications, a restricted form of guarded quantifications described in Fig. 2.4 is also recognized for (possibly infinite) enumerable types (typically, integer). In guarded quantifications, each bound variable must be guarded exactly once and, if its bounds depend on other bound variables, these variables must be guarded earlier or guarded by the same guard. Additionnally, guards are limited to bound variables, meaning that the only allowed identifiers id are variable identifiers enclosed in the binder list. Example 2.1 The following predicates are (labeled) guarded quantifications: – sorted: \forall integer i, j; 0 <= i <= j < len ==> a[i] <= a[j] – is_c: \exists u8 *q; p <= q < p + len && *q == (u8)c Iterator quantification For iterating over other data structures, E-ACSL introduces a notion of iterators over types that are introduced by a specific construct which attaches two sets — namely nexts and guards — to a binary predicate over a type τ . This construct is described by the grammar of Figure 2.5. For a type τ , nexts is a set of terms, and guards a set of predicates of the same cardinal. Each term in nexts is a function taking an argument of type τ and returning a value of type τ which is a successor of its argument. Each 6 2.2. LOGIC EXPRESSIONS literal ::= \true | \false boolean constants | integer (lexical) integer constants | real (lexical) real constants | string (lexical) string constants | character (lexical) character constants bin-op ::= + | - | * | / | % | == | != | <= | >= | > | < | && | || | ^^ boolean operations | << | >> | & | | | --> | <--> | ^ bitwise operations unary-op ::= + | - unary plus and minus | ! boolean negation | ~ bitwise complementation | * pointer dereferencing | & address-of operator term ::= literal literal constants | id variables, function names | unary-op term | term bin-op term | term [ term ] array access | { term \with [ term ] = term } array functional modifier | term . id structure field access | { term \with . id = term } field functional modifier | term -> id | ( type-expr ) term cast | id ( term (, term)∗ ) function application | ( term ) parentheses | term ? term : term ternary condition | \let id = term ; term local binding | sizeof ( term ) | sizeof ( C-type-expr ) | id : term syntactic naming | string : term syntactic naming poly-id ::= id ident ::= id Figure 2.1: Grammar of terms. The terminals id, C-type-name, and various literals are the same as the corresponding C lexical tokens. 7 2.2. LOGIC EXPRESSIONS rel-op ::= == | != | <= | >= | > | < pred ::= \true | \false | term (rel-op term)+ comparisons | id ( term (, term)∗ ) predicate application | ( pred ) parentheses | pred && pred conjunction | pred || pred disjunction | pred ==> pred implication | pred <==> pred equivalence | ! pred negation | pred ^^ pred exclusive or | term ? pred : pred ternary condition | pred ? pred : pred | \let id = term ; pred local binding | \let id = pred ; pred | \forall binders ; integer-guards ==> pred univ. integer quantification | \exists binders ; integer-guards && pred exist. integer quantification | \forall binders ; iterator-guard ==> pred univ. iterator quantification | \exists binders ; iterator-guard && pred exist. iterator quantification | \forall binders ; pred univ. quantification | \exists binders ; pred exist. quantification | id : pred syntactic naming | string : pred syntactic naming integer-guards ::= interv (&& interv)∗ interv ::= (term integer-guard-op)+ id (integer-guard-op term)+ integer-guard-op ::= <= | < iterator-guard ::= id ( term , term ) Figure 2.2: Grammar of predicates 8 2.2. LOGIC EXPRESSIONS binders ::= binder (, binder)∗ binder ::= type-expr variable-ident (,variable-ident)∗ type-expr ::= logic-type-expr | C-type-name logic-type-expr ::= built-in-logic-type | id type identifier built-in-logic-type ::= boolean | integer | real variable-ident ::= id | * variable-ident | variable-ident [] | ( variable-ident ) Figure 2.3: Grammar of binders and type expressions guarded-quantif ::= \forall binders ; (guards ==>)+ pred | \exists binders ; guards && pred guards ::= interv (&& interv)∗ interv ::= term (guard-op id)+ guard-op term guard-op ::= <= | < Figure 2.4: Grammar of guarded quantifications. iterator ::= \forall binders ; iterator-guard ==> pred | \exists binders ; iterator-guard && pred iterator-guard ::= id ( term , term ) declaration ::= //@ iterator id ( wildcard-param , wildcard-param ) : nexts terms ; guards predicates ; wildcard-param ::= parameter | _ terms ::= term (, term)∗ predicates ::= predicate (, predicate)∗ Figure 2.5: Grammar of iterator declarations 9 2.2. LOGIC EXPRESSIONS predicate in the set guards takes an element of type τ , and is valid (resp. invalid) to indicate that the iteration should continue on the corresponding successor (resp. stop at the given argument). Furthermore, the guard of a quantification using an iterator must be the predicate given in the definition of the iterator. This abstract binary predicate takes two arguments of the same type. One of them must be unnamed by using a wildcard (character underscore ’_’). The unnamed argument must be bound to the quantifier, while the other corresponds to the term from which the iteration begins. Example 2.2 The following example introduces binary trees and a predicate which is valid if and only if each value of a binary tree is even. struct btree { int val; struct btree *left, *right; }; /*@ iterator access(_, struct btree *t): @ nexts t->left, t->right; @ guards \valid(t->left), \valid(t->right); */ /*@ predicate is_even(struct btree *t) = @ \forall struct btree *tt; access(tt, t) ==> tt->val % 2 == 0; */ 2.2.1 Operators precedence No difference with ACSL. Figure 2.6 summarizes operator precedences. class associativity operators selection left [· · ·]-> . unary right ! ~ + - * & (cast) sizeof multiplicative left */% additive left +- shift left << >> comparison left < <= > >= comparison left == != bitwise and left & bitwise xor left ^ bitwise or left | bitwise implies left --> bitwise equiv left <--> connective and left && connective xor left ^^ connective or left || connective implies right ==> connective equiv left <==> ternary connective right · · ·?· · ·:· · · binding left \forall \exists \let naming right : Figure 2.6: Operator precedence 10 2.2. LOGIC EXPRESSIONS 2.2.2 Semantics No difference with ACSL, but undefinedness and same laziness than C. More precisely, while ACSL is a 2-valued logic with only total functions, E-ACSL is a 3-valued logic with partial functions since terms and predicates may be “undefined”. In this logic, the semantics of a term denoting a C expression e is undefined if e leads to a runtime error. Consequently the semantics of any term t (resp. predicate p) containing a C expression e leading to a runtime error is undefined if e has to be evaluated in order to evaluate t (resp. p). Example 2.3 The semantics of all the below predicates are undefined: – 1/0 == 1/0 – f(*p) for any logic function f and invalid pointer p Furthermore, C-like operators &&, ||, and _ ? _ : _ are lazy like in C: their right members are evaluated only if required. Thus the amount of undefinedness is limited. Consequently, predicate p ==> q is also lazy since it is equivalent to !p || q. It is also the case for guarded quantifications since guards are conjunctions and for ternary condition since it is equivalent to a disjunction of implications. Example 2.4 All the predicates below are well defined. The first, second and fourth predicates are invalid, whereas the third one is valid: – \false && 1/0 == 1/0 – \forall integer x, -1 <= x <= 1 ==> 1/x > 0 – \forall integer x, 0 <= x <= 0 ==> \false ==> -1 <= 1/x <= 1 – \exists integer x, 1 <= x <= 0 && -1 <= 1/0 <= 1 In particular, the second one is invalid since the quantification is in fact an enumeration over a finite number of elements, it amounts to 1/-1 > 0 && 1/0 > 0 && 1/1 > 0. The first atomic proposition is invalid, so the rest of the conjunction (and in particular 1/0) is not evaluated. The fourth one is invalid since it is an existential quantification over an empty range. A contrario the semantics of the predicates below is undefined: – 1/0 == 1/0 && \false – -1 <= 1/0 <= 1 ==> \true – \exists integer x, -1 <= x <= 1 && 1/x > 0 Furthermore, casting a term denoting a C expression e to a smaller type τ is undefined if e is not representable in τ . Example 2.5 Below, the first term is well-defined, while the second one is undefined. – (char)127 – (char)128 Handling undefinedness in tools It is the responsibility of each tool which interprets E-ACSL to ensure that an undefined term is never evaluated. For instance, it may exit with a proper error message or, if it generates C code, it may guard each generated undefined C expression in order to be sure that they are always safely used. This behavior is consistent with both ACSL [2] and mainstream specification languages for runtime assertion checking like JML [10]. Consistency means that, if it exists and is defined, the E-ACSL predicate corresponding to a valid (resp. invalid) ACSL predicate is valid (resp. invalid). Thus it is possible to reuse tools interpreting ACSL (e.g., Frama-C’s Eva [4] or Wp [1] in order to interpret E-ACSL, and it is also possible to perform runtime assertion checking of E-ACSL predicates in the same way than JML predicates. Reader interested by the implications (especially issues) of such a choice may read the articles of Patrice Chalin on that topic [5, 6]. 11 2.3. FUNCTION CONTRACTS 2.2.3 Typing No difference with ACSL. 2.2.4 Integer arithmetic and machine integers No difference with ACSL. 2.2.5 Real numbers and floating point numbers No difference with ACSL, but no quantification over real numbers and floating point numbers. Exact real numbers and even operations over floating point numbers are usually difficult to implement. Thus, most tools may not support them (or may support them partially). More precisely, most real numbers are not representable at runtime with an infinite precisions. Consequently, most operations over them (e.g., equality) cannot be computed at runtime with an arbitrary precision. In such cases, it is the responsibility of each tool which interprets E-ACSL to specify the level of precision (e.g., 1e−6 ) up to which it is sound, and/or to emit undefinitive verdicts (e.g., “unknown”). 2.2.6 C arrays and pointers No difference with ACSL. Ensuring validity of memory accesses is usually difficult to implement, since it requires the imple- mentation of a memory model. Thus, most tools may not support it (or may support it partially). 2.2.7 Structures, Unions and Arrays in logic No difference with ACSL. Logic arrays without an explicit length are usually difficult to implement. Thus, most tools may not support them (or may support them partially). 2.3 Function contracts No difference with ACSL, but no clause terminates. Figure 2.7 shows the grammar of function contracts. This is a simplified version of ACSL one without terminates clauses. Section 2.5 explains why E-ACSL has no terminates clause. 2.3.1 Built-in constructs \old and \result No difference with ACSL. Figure 2.8 summarizes the grammar extension of terms with \old and \result. 2.3.2 Simple function contracts No difference with ACSL. assigns is usually difficult to implement, since it requires the implementation of a memory model. Thus, most tools may not support it (or may support it partially). 2.3.3 Contracts with named behaviors No difference with ACSL. 12 2.3. FUNCTION CONTRACTS function-contract ::= requires-clause ∗ decreases-clause ? simple-clause ∗ named-behavior ∗ completeness-clause ∗ clause-kind ::= check | admit requires-clause ::= clause-kind ? requires pred ; decreases-clause ::= decreases term (for ident)? ; simple-clause ::= assigns-clause | ensures-clause | allocation-clause | abrupt-clause assigns-clause ::= assigns locations ; locations ::= locations-list | \nothing ∗ locations-list ::= location (, location) location ::= tset ensures-clause ::= clause-kind ? ensures pred ; named-behavior ::= behavior id : behavior-body ∗ behavior-body ::= assumes-clause requires-clause ∗ simple-clause ∗ assumes-clause ::= assumes pred ; completeness-clause ::= complete behaviors (id (, id)∗ )? ; | disjoint behaviors (id (, id)∗ )? ; Figure 2.7: Grammar of function contracts term ::= \old ( term ) old value | \result result of a function pred ::= \old ( pred ) Figure 2.8: \old and \result in terms 13 2.4. STATEMENT ANNOTATIONS 2.3.4 Memory locations and sets of terms No difference with ACSL, but ranges and set comprehensions are limited in order to be finite. Figure 2.9 describes the grammar of sets of terms. There are two differences with ACSL: – ranges necessarily have lower and upper bounds; – a guard for each binder is required when defining set comprehension. The requested constraints for guards are the very same than the ones for quantifications. range ::= term .. term tset ::= \empty empty set | tset -> id | tset . id | * tset | & tset | tset [ tset ] | tset [ range ] | ( range ) a range as a set of integers | \union ( tset (, tset)∗ ) union of location sets | \inter ( tset (, tset)∗ ) intersection of location sets | tset + tset | ( tset ) | { tset | binders ; constraints } set comprehension | { (term (, term)∗ )? } explicit set | term implicit singleton pred ::= \subset ( tset , tset ) set inclusion | term \in tset set membership constraints ::= guards (&& pred)? Figure 2.9: Grammar for sets of terms Example 2.6 The set { x | integer x; 0 <= x <= 10 && x % 2 == 0} denotes the set of even integers between 0 and 10. 2.3.5 Default contracts, multiple contracts No difference with ACSL. 2.4 Statement annotations 2.4.1 Assertions No difference with ACSL. Figure 2.10 summarizes the grammar for assertions. 2.4.2 Loop annotations No difference with ACSL, but loop invariants lose their inductive nature. Figure 2.11 shows the grammar for loop annotations. There is no syntactic difference with ACSL. 14 2.4. STATEMENT ANNOTATIONS C-compound-statement ::= { C-declaration∗ C-statement∗ assertion+ } C-statement ::= assertion C-statement assertion-kind ::= assert assertion | clause-kind non-blocking assertion assertion ::= /*@ assertion-kind pred ; */ | /*@ for id (, id)∗ : assertion-kind pred ; */ Figure 2.10: Grammar for assertions statement ::= /*@ loop-annot */ C-iteration-statement loop-annot ::= loop-clause ∗ loop-behavior ∗ loop-variant? loop-clause ::= loop-invariant | loop-assigns | loop-allocation loop-invariant ::= clause-kind ? loop invariant pred ; loop-assigns ::= loop assigns locations ; loop-behavior ::= for id (, id)∗ : loop-clause ∗ annotation for behavior id loop-variant ::= loop variant term ; | loop variant term for id ; variant for relation id Figure 2.11: Grammar for loop annotations 15 2.4. STATEMENT ANNOTATIONS loop allocation and loop assigns are usually difficult to implement, since they require the implementation of a memory model. Thus, most tools may not support them (or may support them partially). Loop invariants The semantics of loop invariants is the same than the one defined in ACSL, except that they are not inductive. More precisely, if one does not take care of side effects (the semantics of specifications about side effects in loop is the same in E-ACSL than the one in ACSL), a loop invariant I is valid in ACSL if and only if: – I holds before entering the loop; and – if I is assumed true in some state where the loop condition c is also true, and if the execution of the loop body in that state ends normally at the end of the body or with a "continue" statement, I is true in the resulting state. In E-ACSL, the same loop invariant I is valid if and only if: – I holds before entering the loop; and – if the execution of the loop body in that state ends normally at the end of the body or with a "continue" statement, I is true in the resulting state. Thus the only difference with ACSL is that E-ACSL does not assume that the invariant previously holds when one checks that it holds at the end of the loop body. In other words a loop invariant I is equivalent to putting an assertion I just before entering the loop and at the very end of the loop body. Example 2.7 In the following, bsearch(t,n,v) searches for element v in array t between indices 0 and n-1. /*@ requires n >= 0 && \valid(t+(0..n-1)); @ assigns \nothing; @ ensures -1 <= \result <= n-1; @ behavior success: @ ensures \result >= 0 ==> t[\result] == v; @ behavior failure: @ assumes t_is_sorted : \forall integer k1, int k2; @ 0 <= k1 <= k2 <= n-1 ==> t[k1] <= t[k2]; @ ensures \result == -1 ==> @ \forall integer k; 0 <= k < n ==> t[k] != v; @*/ int bsearch(double t[], int n, double v) { int l = 0, u = n-1; /*@ loop invariant 0 <= l && u <= n-1; @ for failure: loop invariant @ \forall integer k; 0 <= k < n ==> t[k] == v ==> l <= k <= u; @*/ while (l <= u ) { int m = l + (u-l)/2; // better than (l+u)/2 if (t[m] < v) l = m + 1; else if (t[m] > v) u = m - 1; else return m; } return -1; } In E-ACSL, this annotated function is equivalent to the following one since loop invariants are not inductive. 16 2.4. STATEMENT ANNOTATIONS /*@ requires n >= 0 && \valid(t+(0..n-1)); @ assigns \nothing; @ ensures -1 <= \result <= n-1; @ behavior success: @ ensures \result >= 0 ==> t[\result] == v; @ behavior failure: @ assumes t_is_sorted : \forall integer k1, int k2; @ 0 <= k1 <= k2 <= n-1 ==> t[k1] <= t[k2]; @ ensures \result == -1 ==> @ \forall integer k; 0 <= k < n ==> t[k] != v; @*/ int bsearch(double t[], int n, double v) { int l = 0, u = n-1; /*@ assert 0 <= l && u <= n-1; @ for failure: assert @ \forall integer k; 0 <= k < n ==> t[k] == v ==> l <= k <= u; @*/ while (l <= u ) { int m = l + (u-l)/2; // better than (l+u)/2 if (t[m] < v) l = m + 1; else if (t[m] > v) u = m - 1; else return m; /*@ assert 0 <= l && u <= n-1; @ for failure: assert @ \forall integer k; 0 <= k < n ==> t[k] == v ==> l <= k <= u; @*/ ; } return -1; } General inductive invariant The syntax of this kind of invariant is shown Figure 2.12. assertion ::= /*@ clause-kind ? invariant pred ; */ | /*@ for id (, id)∗ : clause-kind ? invariant pred ; */ Figure 2.12: Grammar for general inductive invariants In E-ACSL, a general inductive invariant may be written everywhere in a loop body, and is exactly equivalent to writing an assertion. 2.4.3 Built-in construct \at No difference with ACSL, but no forward references. The construct \at(t,id) (where id is a regular C label, a label added within a ghost statement or a default logic label) follows the same rule than its ACSL counterpart, except that a more restrictive scoping rule must be respected in addition to the standard ACSL scoping rule: – when evaluating \at(t,id) at a propram point p, the program point p′ denoted by id must be reached before p in the program execution flow; and 17 2.4. STATEMENT ANNOTATIONS – when evaluating \at(t,id), for each C left-value x that contributes to the definition of a (non- ghost) logic variable involved in t, the equality \at(x,id) == \at(x,Here) must hold, i.e. the value of x must not be modified between the program points id and Here. Below, the first example illustrates the first constraint, whereas the second example illustrates the second constraint. Example 2.8 In the following example, both assertions are accepted and valid in ACSL, but only the first one is accepted and valid in E-ACSL since evaluating the term \at(*(p+\at(*q,Here)),L1) at L2 requires to evaluate the term \at(*q,Here) at L1: that is forbidden since L1 is executed before L2. /*@ requires \valid(p+(0..1)); @ requires \valid(q); @*/ void f(int *p, int *q) { *p = 0; *(p+1) = 1; *q = 0; L1: *p = 2; *(p+1) = 3; *q = 1; L2: /*@ assert (\at(*(p+\at(*q,L1)),Here) == 2); */ /*@ assert (\at(*(p+\at(*q,Here)),L1) == 1); */ return ; } Example 2.9 In the following example, the first assertion is supported, while the second one is not supported. Indeed, in the second assertion, the guard defining the logic variable u depends on n whose value is modified between L1 and L2. main(void) { int m = 2; int n = 7;; L1: ; n = 4; L2: /*@ assert \let k = m + 1; \exists integer u; 9 <= u < 21 && \forall integer v; -5 < v <= (u < 15 ? u + 6 : k) ==> \at(n + u + v > 0, K); */ ; /*@ assert \let k = m + 1; \exists integer u; n <= u < 21 && // [u] depends on [n] \forall integer v; -5 < v <= (u < 15 ? u + 6 : k) ==> \at(n + u + v > 0, L1); */ ; return 0; } 2.4.4 Statement contracts No difference with ACSL. Figure 2.13 shows the grammar of statement contracts. 18 2.5. TERMINATION statement ::= /*@ statement-contract */ statement statement-contract ::= (for id (, id)∗ :)? requires-clause ∗ simple-clause-stmt∗ named-behavior-stmt∗ completeness-clause ∗ simple-clause-stmt ::= simple-clause | abrupt-clause-stmt named-behavior-stmt ::= behavior id : behavior-body-stmt ∗ behavior-body-stmt ::= assumes-clause requires-clause ∗ simple-clause-stmt∗ Figure 2.13: Grammar for statement contracts 2.5 Termination No difference with ACSL, but no terminates clauses. 2.5.1 Integer measures No difference with ACSL. 2.5.2 General measures No difference with ACSL. 2.5.3 Recursive function calls No difference with ACSL. 2.5.4 Non-terminating functions No such feature in E-ACSL: whether a function is guaranteed to terminate if some predicate p holds is not a monitorable property. 2.6 Logic specifications No difference with ACSL. Figure 2.14 presents the grammar of logic definitions. 2.6.1 Predicate and function definitions No difference with ACSL. 2.6.2 Lemmas No difference with ACSL. Lemmas are verified before running the function main but after initializing global variables. 19 2.6. LOGIC SPECIFICATIONS C-external-declaration ::= /*@ logic-def + */ logic-def ::= logic-const-def | logic-function-def | logic-predicate-def | lemma-def | data-inv-def type-var ::= id type-expr ::= type-var type variable | id < type-expr (, type-expr)∗ > polymorphic type type-var-binders ::= < type-var (, type-var)∗ > poly-id ::= id type-var-binders polymorphic object identifier logic-const-def ::= logic type-expr poly-id = term ; logic-function-def ::= logic type-expr poly-id parameters = term ; logic-predicate-def ::= predicate poly-id parameters ? = pred ; parameters ::= ( parameter (, parameter)∗ ) parameter ::= type-expr id lemma-def ::= clause-kind ? lemma poly-id : pred ; Figure 2.14: Grammar for global logic definitions 20 2.6. LOGIC SPECIFICATIONS 2.6.3 Inductive predicates Experimental No difference with ACSL. Figure 2.15 presents the grammar of inductive predicates. logic-def ::= inductive-def inductive-def ::= inductive poly-id parameters ? { indcase ∗ } indcase ::= case poly-id : pred ; Figure 2.15: Grammar for inductive predicates Inductive predicates in all their generality are not monitorable. Therefore, future versions of this document will restrict them syntactically (e.g., to definite Horn clauses (http://en.wikipedia. org/wiki/Horn_clause) and/or through semantic criteria. 2.6.4 Axiomatic definitions Experimental No difference with ACSL. Figure 2.16 presents the grammar of axiomatic definitions. logic-def ::= axiomatic-decl axiomatic-decl ::= axiomatic id { logic-decl ∗ } logic-decl ::= logic-def | logic-type-decl | logic-const-decl | logic-predicate-decl | logic-function-decl | axiom-def logic-type-decl ::= type logic-type ; logic-type ::= id | id type-var-binders polymorphic type logic-const-decl ::= logic type-expr poly-id ; logic-function-decl ::= logic type-expr poly-id parameters ; logic-predicate-decl ::= predicate poly-id parameters ? ; axiom-def ::= axiom poly-id : pred ; Figure 2.16: Grammar for axiomatic declarations Axiomatic definitions in all their generality are not monitorable. Therefore, future versions of this document will restrict them syntactically and/or through semantic criteria. 21 2.6. LOGIC SPECIFICATIONS 2.6.5 Polymorphic logic types No difference with ACSL. 2.6.6 Recursive logic definitions No difference with ACSL. 2.6.7 Higher-order logic constructions Experimental No difference with ACSL. Figure 2.17 introduces new term constructs for higher-order logic. term ::= \lambda binders ; term abstraction | ext-quantifier ( term , term , term ) | { term \with [ range ] = term } ext-quantifier ::= \max | \min | \sum | \product | \numof Figure 2.17: Grammar for higher-order constructs Abstractions are only implemented for extended quantifiers, such as the term \sum(1, 10, \lambda integer k; k). 2.6.8 Concrete logic types Experimental No difference with ACSL. Figure 2.18 introduces new constructs for defining logic types and the associated new terms. 2.6.9 Hybrid functions and predicates No difference with ACSL. Hybrid functions and predicates are usually difficult to implement, since they require the implementa- tion of a memory model (or at least to support \at). Thus, most tools may not support them (or may support them partially). 2.6.10 Memory footprint specification: reads clause Experimental No difference with ACSL. Figure 2.19 introduces reads clauses. read clauses are usually difficult to implement, since they require the implementation of a memory model. Thus, most tools may not support them (or may support them partially). 2.6.11 Specification Modules No difference with ACSL. 22 2.6. LOGIC SPECIFICATIONS logic-def ::= type logic-type = logic-type-def ; logic-type-def ::= record-type | sum-type | product-type | function-type | type-expr type abbreviation record-type ::= { type-expr id ( ; type-expr id)∗ ;? } function-type ::= ( ( type-expr (, type-expr )∗ )? ) -> type-expr sum-type ::= |? constructor ( | constructor)∗ constructor ::= id constant constructor | id ( type-expr (, type-expr)∗ ) non-constant constructor product-type ::= ( type-expr (, type-expr)+ ) product type term ::= term . id record field access | \match term { match-cases } pattern-matching | ( term (, term)+ ) tuples | { (. id = term ;)+ } records | \let ( id (, id)+ ) = term ; term match-cases ::= match-case + match-case ::= case pat : term pat ::= id constant constructor | id ( pat ( , pat)∗ ) non-constant constructor | pat | pat or pattern | _ any pattern | literal | { (. id = pat)∗ } record pattern | ( pat ( , pat )∗ ) tuple pattern | pat as id pattern binding Figure 2.18: Grammar for concrete logic types and pattern-matching 23 2.7. POINTERS AND PHYSICAL ADRESSING logic-function-decl ::= logic type-expr poly-id parameters reads-clause ; logic-predicate-decl ::= predicate poly-id parameters ? reads-clause ; reads-clause ::= reads locations logic-function-def ::= logic type-expr poly-id parameters reads-clause = term ; logic-predicate-def ::= predicate poly-id parameters ? reads-clause = pred ; Figure 2.19: Grammar for logic declarations with reads clauses 2.7 Pointers and physical adressing No difference with ACSL. Figure 2.20 shows the additional constructs for terms and predicates which are related to memory location. term ::= \null | \base_addr one-label ? ( term ) | \block_length one-label ? ( term ) | \offset one-label ? ( term ) | \allocation one-label ? ( term ) pred ::= \allocable one-label ? ( term ) | \freeable one-label ? ( term ) | \fresh two-labels ? ( term, term ) | \valid one-label ? ( locations-list ) | \valid_read one-label ? ( locations-list ) | \separated ( location , locations-list ) | \object_pointer one-label ? ( locations-list ) | \pointer_comparable one-label ? ( term , term ) one-label ::= { label-id } two-labels ::= { label-id, label-id } Figure 2.20: Grammar extension of terms and predicates about memory 2.7.1 Memory blocks and pointer dereferencing No difference with ACSL. All memory-related built-in functions and predicates are usually difficult to implement, since they require the implementation of a memory model. Thus, most tools may not support them (or may support them partially). 24 2.8. SETS AND LISTS 2.7.2 Separation No difference with ACSL. \separated is usually difficult to implement, since it requires the implementation of a memory model. Thus, most tools may not support it (or may support it partially). 2.7.3 Dynamic allocation and deallocation No difference with ACSL. All these constructs are usually difficult to implement, since they require the implementation of a memory model. Thus, most tools may not support them (or may support them partially). Figure 2.21 introduces grammar for dynamic allocations and deallocations. allocation-clause ::= allocates dyn-allocation-addresses ; | frees dyn-allocation-addresses ; loop-allocation ::= loop allocates dyn-allocation-addresses ; | loop frees dyn-allocation-addresses ; dyn-allocation-addresses ::= locations Figure 2.21: Grammar for dynamic allocations and deallocations 2.8 Sets and lists 2.8.1 Finite sets No difference with ACSL. 2.8.2 Finite lists No difference with ACSL. Figure 2.22 shows the notations for built-in lists. 2.9 Abrupt termination No difference with ACSL. Figure 2.23 shows the grammar of abrupt terminations. 2.10 Dependencies information Experimental No difference with ACSL. Figure 2.24 shows the grammar for dependencies information. 25 2.11. DATA INVARIANTS term ::= [| |] empty list | [| term (, term)∗ |] list of elements | term ^ term list concatenation (overloading bitwise-xor operator) | term *^ term list repetition Figure 2.22: Notations for built-in list datatype abrupt-clause ::= exits-clause exits-clause ::= exits pred ; abrupt-clause-stmt ::= breaks-clause | continues-clause | returns-clause exits-clause breaks-clause ::= breaks pred ; continues-clause ::= continues pred ; returns-clause ::= returns pred ; term ::= \exit_status Figure 2.23: Grammar of contracts about abrupt terminations 2.11 Data invariants No difference with ACSL. Figure 2.25 summarizes grammar for declarations of data invariants. strong invariants are unlikely evaluated efficiently at runtime. 2.11.1 Semantics No difference with ACSL. 2.11.2 Model variables and model fields No difference with ACSL. Figure 2.26 summarizes the grammar for declarations of model variables and fields. 2.12 Ghost variables and statements No difference with ACSL. Figure 2.27 summarizes the grammar for ghost statements which is the same than the one of ACSL. 2.12.1 Volatile variables Figure 2.28 summarizes the grammar for volatile constructs. 26 2.13. INITIALIZATION AND UNDEFINED VALUES assigns-clause ::= assigns locations-list (\from locations )? ; | assigns term \from locations = term ; Figure 2.24: Grammar for dependencies information data-inv-def ::= data-invariant | type-invariant data-invariant ::= inv-strength? global invariant id : pred ; type-invariant ::= inv-strength? type invariant id ( C-type-name id ) = pred ; inv-strength ::= weak | strong Figure 2.25: Grammar for declarations of data invariants 2.13 Initialization and undefined values No difference with ACSL. \initialized is usually difficult to implement, since it requires the implementation of a memory model. Thus, most tools may not support it (or may support it partially). 2.14 Dangling pointers No difference with ACSL. \dangling is usually difficult to implement, since it requires the implementation of a memory model. Thus, most tools may not support it (or may support it partially). 2.15 Well-typed pointers No such feature in E-ACSL: it would require the implementation of a C type system at runtime. 2.16 Logic attribute annotations No such feature in E-ACSL: logic attributes are implementation dependent; therefore their meaning cannot be guessed by a general-purpose (runtime) verification tool. logic-def ::= model parameter ; model variable | model C-type-name { parameter ;? } ; model field Figure 2.26: Grammar for declarations of model variables and fields 27 2.16. LOGIC ATTRIBUTE ANNOTATIONS C-type-qualifier ::= \ghost only in ghost C-type-specifier ::= logic-type logic-def ::= ghost C-declaration C-direct-declarator ::= C-direct-declarator function declarator ( C-parameter-type-list? ) /*@ ghost ( C-parameter-type-list with ghost params ) */ C-postfix-expression ::= C-postfix-expression function call ( C-argument-expression-list? ) /*@ ghost ( C-argument-expression-list with ghost args ) */ C-statement ::= /*@ ghost C-statement+ ghost code */ | if ( C-expression ) statement /*@ ghost else C-statement ghost alternative C-statement∗ unconditional ghost code */ C-struct-declaration ::= /*@ ghost C-struct-declaration ghost field */ Figure 2.27: Grammar for ghost statements logic-def ::= //@ volatile locations (reads ident)? (writes ident)? ; Figure 2.28: Grammar for volatile constructs 28 2.17. PREPROCESSING FOR ACSL 2.17 Preprocessing for ACSL No difference with ACSL. 29 Libraries 3 Disclaimer: this chapter is empty on purpose. It is left here to be consistent with the ACSL reference manual [2]. 30 Conclusion 4 This document presents an Executable ANSI/ISO C Specification Language. It provides a subset of ACSL [2] implemented [3] in the Frama-C platform [7] in which each construct may be evaluated at runtime. The specification language described here is intended to evolve in the future in two directions. First it is based on ACSL which is itself still evolving. Second the considered subset of ACSL may also change. 31 Appendices A A.1 Changes Version 1.19 – Update according to ACSL 1.19 – Section 2.7.1: add the \object_pointer and \pointer_comparable built-in predi- cates. Version 1.18 – No changes: changes in ACSL 1.18 do not impact E-ACSL. Version 1.17 – Section 2.2: xor ^^ is not lazy. – Section 2.2: new extended syntax for quantifications. – Section 2.2.5: additional remark about real numbers and operations over them. – Section 2.3.4: new extended syntax for set comprehensions. – Section 2.4.3: more restrictive scoping rule for \at constructs. – Section 2.6: add lemmas and data invariants. – Section 2.6.3: add inductive predicates experimentally: the accepted subset will be refined in a future version. – Section 2.6.4: add axiomatic declarations experimentally: the accepted subset will be refined in a future version. – Section 2.6.5: add polymorphic logic types. – Section 2.6.7: add higher-order logic constructions. – Section 2.6.8: add concrete logic types. – Section 2.6.10: add read clauses. – Section 2.10: add dependencies information. – Section 2.12.1: add volatile constructs. Version 1.16 – Update according to ACSL 1.16 – Section 2.3: add the check and admit clause kinds. – Section 2.4.1: add the check and admit clause kinds. – Section 2.4.2: add the check and admit clause kinds. – Section 2.4.2: add the check and admit clause kinds. 32 A.1. CHANGES Version 1.15 – Update according to ACSL 1.15: – Section 2.12: add the \ghost qualifier. Version 1.14 – Update according to ACSL 1.14: – Section 2.4.1: add the keyword check. Version 1.13 – Update according to ACSL 1.13: – Section 2.3.4: add syntax for set membership. Version 1.12 – Update according to ACSL 1.12: – Section 2.3.4: add subsections for build-in lists. – Section 2.4.4: fix syntax rule for statement contracts in allowing completeness clauses. – Section 2.7.1: add syntax for defining a set by giving explicitly its element. – Section 2.15: new section. Version 1.9 – Section 2.7.3: new section. – Update according to ACSL 1.9. Version 1.8 – Section 2.3.4: fix example 2.6. – Section 2.7: add grammar of memory-related terms and predicates. Version 1.7 – Update according to ACSL 1.7. – Section 2.7.2: no more absent. Version 1.5-4 – Fix typos. – Section 2.2: fix syntax of guards in iterators. – Section 2.2.2: fix definition of undefined terms and predicates. – Section 2.2.3: no user-defined types. – Section 2.3.1: no more implementation issue for \old. – Section 2.4.3: more restrictive scoping rule for label references in \at. Version 1.5-3 – Fix various typos. – Warn about features known to be difficult to implement. – Section 2.2: fix semantics of ternary operator. 33 A.1. CHANGES – Section 2.2: fix semantics of cast operator. – Section 2.2: improve syntax of iterator quantifications. – Section 2.2.2: improve and fix example 2.4. – Section 2.4.2: improve explanations about loop invariants. – Section 2.6.9: add hybrid functions and predicates. Version 1.5-2 – Section 2.2: remove laziness of operator <==>. – Section 2.2: restrict guarded quantifications to integer. – Section 2.2: add iterator quantifications. – Section 2.2: extend unguarded quantifications to char. – Section 2.3.4: extend syntax of set comprehensions. – Section 2.4.2: simplify explanations for loop invariants and add example.. Version 1.5-1 – Fix many typos. – Highlight constructs with semantic changes in grammars. – Explain why unsupported features have been removed. – Indicate that experimental ACSL features are unsupported. – Add operations over memory like \valid. – Section 2.2: lazy operators &&, ||, ^^, ==> and <==>. – Section 2.2: allow unguarded quantification over boolean. – Section 2.2: revise syntax of \exists. – Section 2.2.2: better semantics for undefinedness. – Section 2.3.4: revise syntax of set comprehensions. – Section 2.4.2: add loop invariants, but they lose their inductive ACSL nature. – Section 2.5.2: add general measures for termination. – Section 2.6.11: add specification modules. Version 1.5-0 – Initial version. 34 Bibliography [1] Patrick Baudin, François Bobot, Loïc Correnson, Zaynah Dargaye, and Allan Blanchard. Wp Plug-in Manual. https://frama-c.com/fc-plugins/wp.html. [2] Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL, ANSI/ISO C Specification Language. https://frama-c. com/html/acsl.html. [3] Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL, Implementation in Frama-C. https://frama-c.com/ download/frama-c-acsl-implementation.pdf. [4] David Bühler, Pascal Cuoq, Boris Yakobowski, Matthieu Lemerre, André Maroneze, Valentin Perelle, and Virgile Prevosto. Eva — The Evolved Value Analysis Plug-in. https://frama-c. com/fc-plugins/eva.html. [5] Patrice Chalin. Reassessing JML’s logical foundation. In Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs (FTfJP’05), Glasgow, Scotland, July 2005. [6] Patrice Chalin. A sound assertion semantics for the dependable systems evolution verifying compiler. In Proceedings of the International Conference on Software Engineering (ICSE’07), pages 23–33, Los Alamitos, CA, USA, 2007. IEEE Computer Society. [7] Loïc Correnson, Pascal Cuoq, Florent Kirchner, André Maroneze, Virgile Prevosto, Armand Puccetti, Julien Signoles, and Boris Yakobowski. Frama-C User Manual. https://frama-c. com/download/frama-c-user-manual.pdf. [8] International Organization for Standardization (ISO). The ANSI C standard (C99). http: //www.open-std.org/JTC1/SC22/WG14/www/docs/n1124.pdf. [9] Brian Kernighan and Dennis Ritchie. The C Programming Language (2nd Ed.). Prentice-Hall, 1988. [10] Gary T. Leavens, K. Rustan M. Leino, Erik Poll, Clyde Ruby, and Bart Jacobs. JML: notations and tools supporting detailed design in Java. In OOPSLA 2000 Companion, Minneapolis, Minnesota, pages 105–106, 2000. 35 List of Figures 2.1 Grammar of terms. The terminals id, C-type-name, and various literals are the same as the corresponding C lexical tokens. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.2 Grammar of predicates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.3 Grammar of binders and type expressions . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.4 Grammar of guarded quantifications. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.5 Grammar of iterator declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.6 Operator precedence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.7 Grammar of function contracts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.8 \old and \result in terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.9 Grammar for sets of terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.10 Grammar for assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.11 Grammar for loop annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.12 Grammar for general inductive invariants . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.13 Grammar for statement contracts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.14 Grammar for global logic definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2.15 Grammar for inductive predicates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.16 Grammar for axiomatic declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.17 Grammar for higher-order constructs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.18 Grammar for concrete logic types and pattern-matching . . . . . . . . . . . . . . . . . . 23 2.19 Grammar for logic declarations with reads clauses . . . . . . . . . . . . . . . . . . . . . 24 2.20 Grammar extension of terms and predicates about memory . . . . . . . . . . . . . . . . 24 2.21 Grammar for dynamic allocations and deallocations . . . . . . . . . . . . . . . . . . . . 25 2.22 Notations for built-in list datatype . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.23 Grammar of contracts about abrupt terminations . . . . . . . . . . . . . . . . . . . . . . 26 2.24 Grammar for dependencies information . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.25 Grammar for declarations of data invariants . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.26 Grammar for declarations of model variables and fields . . . . . . . . . . . . . . . . . . . 27 2.27 Grammar for ghost statements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2.28 Grammar for volatile constructs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 36 Index ?, 6, 7 for, 12, 14, 16, 18 _, 8, 22 \forall, 7, 8 \freeable, 23 abrupt termination, 24 frees, 24 admit, 12 \fresh, 23 \allocable, 23 \from, 26 allocates, 24 function behavior, 11 \allocation, 23 function contract, 11 annotation, 13 as, 22 ghost, 25 assert, 13, 14 ghost, 27 assigns, 12, 14, 26 \ghost, 27 assumes, 12 global, 26 \at, 16 global invariant, 25 axiom, 20 grammar entries axiomatic, 20 C-compound-statement, 14 C-direct-declarator, 27 \base_addr, 23 C-external-declaration, 19 behavior, 11 C-postfix-expression, 27 behavior, 12, 18 C-statement, 14, 27 behaviors, 12 C-struct-declaration, 27 \block_length, 23 C-type-qualifier, 27 boolean, 8 C-type-specifier, 27 breaks, 25 abrupt-clause-stmt, 25 abrupt-clause, 25 case, 20, 22 allocation-clause, 24 check, 12 assertion-kind, 14 complete, 12 assertion, 14, 16 continues, 25 assigns-clause, 12, 26 contract, 11, 17 assumes-clause, 12 data invariant, 25 axiom-def, 20 decreases, 12 axiomatic-decl, 20 \decreases, 18 behavior-body-stmt, 18 disjoint, 12 behavior-body, 12 bin-op, 6 else, 27 binders, 8 \empty, 13 binder, 8 ensures, 12 breaks-clause, 25 \exists, 7, 8 built-in-logic-type, 8 \exit_status, 25 clause-kind, 12 exits, 25 completeness-clause, 12 constraints, 13 \false, 6, 7 constructor, 22 37 INDEX continues-clause, 25 parameters, 19 data-inv-def, 26 parameter, 19 data-invariant, 26 pat, 22 declaration, 8 poly-id, 6, 19 decreases-clause, 12 predicates, 8 dyn-allocation-addresses, 24 pred, 7, 12, 13, 23 ensures-clause, 12 product-type, 22 exits-clause, 25 range, 13 ext-quantifier, 21 reads-clause, 23 function-contract, 12 record-type, 22 function-type, 22 rel-op, 7 guard-op, 8 requires-clause, 12 guarded-quantif, 8 returns-clause, 25 guards, 8 simple-clause-stmt, 18 ident, 6 simple-clause, 12 indcase, 20 statement-contract, 18 inductive-def, 20 statement, 14, 18 integer-guard-op, 7 sum-type, 22 integer-guards, 7 terms, 8 interv, 7, 8 term, 6, 12, 21–23, 25 inv-strength, 26 tset, 13 iterator-guard, 7, 8 two-labels, 23 iterator, 8 type-expr, 8, 19 lemma-def, 19 type-invariant, 26 literal, 6 type-var-binders, 19 locations-list, 12 type-var, 19 locations, 12 unary-op, 6 location, 12 variable-ident, 8 logic-const-decl, 20 wildcard-param, 8 logic-const-def, 19 guards, 8 logic-decl, 20 logic-def, 19, 20, 22, 26, 27 hybrid logic-function-decl, 20, 23 function, 21 logic-function-def, 19, 23 predicate, 21 logic-predicate-decl, 20, 23 logic-predicate-def, 19, 23 if, 27 logic-type-decl, 20 \in, 13 logic-type-def, 22 inductive, 20 logic-type-expr, 8 inductive predicates, 20 logic-type, 20 integer, 8 loop-allocation, 24 \inter, 13 loop-annot, 14 invariant, 15 loop-assigns, 14 data, 25 loop-behavior, 14 global, 25 loop-clause, 14 type, 25 loop-invariant, 14 invariant, 14, 16, 26 loop-variant, 14 iterator, 8 match-cases, 22 \lambda, 21 match-case, 22 lemma, 19 named-behavior-stmt, 18 \let, 6, 7, 22 named-behavior, 12 location, 24 one-label, 23 logic, 19, 20, 23 38 INDEX logic specification, 18 volatile, 25, 27 loop, 14, 24 weak, 26 \match, 22 \with, 6, 21 \max, 21 writes, 27 \min, 21 model, 25 model, 26 nexts, 8 \nothing, 12 \null, 23 \numof, 21 \object_pointer, 23 \offset, 23 \old, 12 \pointer_comparable, 23 polymorphism, 21 predicate, 19, 20, 23 \product, 21 reads, 23, 27 real, 8 recursion, 21 requires, 12 \result, 12 returns, 25 \separated, 23 sizeof, 6 specification, 18 statement contract, 17 strong, 26 \subset, 13 \sum, 21 termination, 18 \true, 6, 7 type concrete, 21 polymorphic, 21 record, 22 sum, 22 type, 20, 22, 26 type invariant, 25 \union, 13 \valid, 23 \valid_read, 23 variant, 14 \variant, 18 39