ACSL Language Reference (811287), страница 2
Текст из файла (страница 2)
ACSL is an acronym for “ANSI/ISO CSpecification Language”. This is a Behavioral Interface Specification Language (BISL) implemented in the Frama-C framework. It aims at specifying behavioral properties of Csource code. The main inspiration for this language comes from the specification language ofthe Caduceus tool [9, 10] for deductive verification of behavioral properties of C programs.The specification language of Caduceus is itself inspired from the Java Modeling Language(JML [18]) which aims at similar goals for Java source code: indeed it aims both at runtimeassertion checking and static verification using the ESC/Java2 tool [14], where we aim atstatic verification and deductive verification (see Appendix A.2 for a detailed comparisonbetween ACSL and JML).Going back further in history, JML design was guided by the general design-by-contractprinciple proposed by Bertrand Meyer, who took his own inspiration from the concepts ofpreconditions and postconditions on a routine, going back at least to Dijkstra, Floyd andHoare in the late 60’s and early 70’s, and originally implemented in the Eiffel language.In this document, we assume that the reader has a good knowledge of the ISO C programminglanguage [13, 12].1.1Organization of this documentIn this preliminary chapter we introduce some definitions and vocabulary, and discuss generalities about this specification language.
Chapter 2 presents the specification language itself.Chapter 3 presents additional information about libraries of specifications. Appendix A provides specific hindsight over type-checking ACSL annotations, the relation between ACSLand JML, and specification templates. A detailed table of contents is given on page 5. Aglossary is given in Appendix A.1.1.2Generalities about AnnotationsIn this document, we consider that specifications are given as annotations in comments written directly in C source files, so that source files remain compilable. Those comments muststart by /*@ or //@ and end as usual in C.In some contexts, it is not possible to modify the source code. It is strongly recommended thata tool which implements ACSL specifications provides technical means to store annotations11CHAPTER 1.
INTRODUCTIONseparately from the source. It is not the purpose of this document to describe such means.Nevertheless, some of the specifications, namely those at a global level, can be given inseparate files: logical specifications can be imported (see Section 2.6.11) and a functioncontract can be attached to a copy of the function profile (see Section 2.3.5).1.2.1Kinds of annotations• Global annotations:– function contract : such an annotation is inserted just before the declaration orthe definition of a function. See section 2.3.– global invariant : this is allowed at the level of global declarations.
See section 2.11.– type invariant : this allows to declare both structure or union invariants, andinvariants on type names introduced by typedef . See section 2.11.– logic specifications : definitions of logic functions or predicates, lemmas, axiomatizations by declaration of new logic types, logic functions, predicates with axiomsthey satisfy. Such an annotation is placed at the level of global declarations. Seesection 2.6• Statement annotations:– assertion : these are allowed everywhere a C label is allowed, or just before a blockclosing brace. See section 2.4.1.– loop annotation (invariant, variant, assign clauses): is allowed immediately beforea loop statement: for , while , do .
. . while . See Section 2.4.2.– statement contract : very similar to a function contract, and placed before a statement or a block. Semantic conditions must be checked (no goto going inside, nogoto going outside). See Section 2.4.4.– ghost code : regular C code, only visible from the specifications, that is only allowedto modify ghost variables. See section 2.12. This includes ghost braces for enclosingblocks.1.2.2Parsing annotations in practiceIn JML, parsing is done by simply ignoring //@, /*@ and */ at the lexical analysis level. Thistechnique could modify the semantics of the code, for example:1return x /*@ +1 */ ;In our language, this is forbidden.
Technically, the current implementation of Frama-Cisolates the comments in a first step of syntax analysis, and then parses a second time.Nevertheless, the grammar and the corresponding parser must be carefully designed to avoidinteraction of annotations with the code. For example, in code such as12if (c) //@ assert P;c=1;the statement c=1 must be understood as the branch of the if. This is ensured by thegrammar below, saying that assert annotations are not statements themselves, but attachedto the statement that follows, like C labels.121.3.
NOTATIONS FOR GRAMMARS1.2.3About preprocessingThis document considers C source after preprocessing. Tools must decide how they handlepreprocessing (what to do with annotations, whether macro substitution should be performed,etc.)1.2.4About keywordsAdditional keywords of the specification language start with a backslash, if they are used inthe position of a term or a predicate (which are defined in the following). Otherwise they donot start with a backslash (like ensures ) and they remain valid identifiers.1.3Notations for grammarsIn this document, grammar rules are given in BNF form. In grammar rules, we use extranotations e∗ to denote repetition of zero, one or more occurrences of e, e+ for repetition of oneor more occurrences of e, and e? for zero or one occurrence of e.
For the sake of simplicity, weonly describe annotations in the usual /*@ ... */ style of comments. One-line annotationsin //@ comments are alike.13Chapter 2Specification language2.1Lexical rulesLexical structure mostly follows that of ANSI/ISO C. A few differences must be noted.• The at sign (@) is a blank character, thus equivalent to a space character.• Identifiers may start with the backslash character (\).• Some UTF8 characters may be used in place of some constructs, as shown in thefollowing table:>=<=><!=====><==>&&||^^ (xor)!- (unary minus)\forall\existsintegerrealboolean≥≤><6≡≡=⇒⇐⇒∧∨∨¬−∀∃ZRB0x22650x22640x003E0x003C0x22620x22610x21D20x21D40x22270x22280x22BB0x00AC0x22120x22000x22030x21240x211D0x1D539• Comments can be put inside ACSL annotations. They use the C++ format, i.e.
beginwith // and extend to the end of current line.15CHAPTER 2. SPECIFICATION LANGUAGEliteral::=||||\true | \falseintegerrealstringcharacterboolean constantsinteger constantsreal constantsstring constantscharacter constantsbin-op::=|||+ | - | * | / | % | << | >>== | != | <= | >= | > | <&& | || | ^^& | | | --> | <--> | ^boolean operationsbitwise operationsunary-op::=||||+ |!~*&unary plus and minusboolean negationbitwise complementationpointer dereferencingaddress-of operatorterm::=|||||||||||||||||literalpoly-idunary-op termterm bin-op termterm [ term ]{ term \with [ term ] = termterm . id{ term \with . id = term }term -> id( type-expr ) termpoly-id ( term (, term)∗ )( term )term ? term : term\let id = term ; termsizeof ( term )sizeof ( C-type-name )id : termstring : term::=identpoly-id-literal constantsvariables}array accessarray functional modifierstructure field accessfield functional modifiercastfunction applicationparenthesesternary conditionlocal bindingsyntactic namingsyntactic namingnormal identifierFigure 2.1: Grammar of terms2.2Logic expressionsThis first section presents the language of expressions one can use in annotations.
Theseare called logic expressions in the following. They correspond to pure C expressions, withadditional constructs that we will introduce progressively.Figures 2.1 and 2.2 present the grammar for the basic constructs of logic expressions.
Inthat grammar, we distinguish between predicates and terms, following the usual distinctionbetween propositions and terms in classical first-order logic. 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 ; x can then be usedin expression 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.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
