ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver (1185160), страница 9
Текст из файла (страница 9)
These declarations follows the47CHAPTER 2. SPECIFICATION LANGUAGEC-external-declaration::=/*@ logic-def +logic-def::=|||logic-const-deflogic-function-deflogic-predicate-deflemma-decltype-var::=idtype-expr::=|type-varid< type-expr(, type-expr)∗type-var-binders::=logic-const-deflogic-function-deflogic-predicate-deftype variable>>::=|idid::=logic type-exprpoly-id = term::=::=polymorphic type< type-var(, type-var)∗poly-id*/type-var-binders;logic type-exprpoly-id parametersterm ;::==predicatepoly-id parameters ?pred ;parametersnormal identifierpolymorphic object identifier=( parameter(, parameter)∗parameter::=type-exprlemma-decl::=lemma poly-idpred ;)id:Figure 2.12: Grammar for global logic definitionsclassical setting of algebraic specifications. The grammar for these declarations is given inFigure 2.12.2.6.1Predicate and function definitionsNew functions and predicates can be defined by explicit expressions, given after an equalsign.Example 2.37 The following definitions1234//@ predicate is_positive(integer x) = x > 0;/*@ logic integer get_sign(real x) =@ x > 0.0 ? 1 : ( x < 0.0 ? -1 : 0);@*/482.6.
LOGIC SPECIFICATIONSlogic-def::=inductive-definductive-def::=inductivepoly-idindcase::=parameters ?case poly-id: pred{ indcase ∗};Figure 2.13: Grammar for inductive definitionsillustrates the definition of a new predicate is_positive with an integer parameter, and a newlogic function sign with a real parameter returning an integer.2.6.2LemmasLemmas are user-given propositions, a facility that might help theorem provers to establishvalidity of ACSL specifications.Example 2.38 The following lemma1//@ lemma mean_property: \forall integer x,y; x <= y ==> x <= (x+y)/2 <= y;is a useful hint for program like binary search.Of course, a complete verification of an ACSL specification has to provide a proof for eachlemma.2.6.3Inductive predicatesA predicate may also be defined by an inductive definition.
The grammar for those style ofdefinitions is given on Figure 2.13.In general, an inductive definition of a predicate P has the form123456/*@ inductive P(x1 ,. . .,xn ) {@ case c1 : p1 ;...@ case ck : pk ;@ }@*/where each ci is an identifier and each pi is a proposition.The semantics of such a definition is that P is the least fixpoint of the cases, i.e. is thesmallest predicate (in the sense that it is false the most often) satisfying the propositionsp1 , . .
. ,pk . With this general form, the existence of a least fixpoint is not guaranteed, so toolsmight enforce syntactic conditions on the form of inductive definitions. A standard syntacticrestriction could be to allow only propositions pi of the form\forall y1 ,...,ym , h1 ==> · · · ==> hl ==> P(t1 ,...,tn )where P occurs only positively in hypotheses h1 , . .
. ,hl (definite Horn clauses, http://en.wikipedia.org/wiki/Horn_clause).Example 2.39 The following introduce a predicate isgcd(x,y,d) meaning that d is the greatest common divisor of x and y.49CHAPTER 2. SPECIFICATION LANGUAGElogic-def::=axiomatic-declaxiomatic-decl::=axiomatic idlogic-decl::=|||||logic-deflogic-type-decllogic-const-decllogic-predicate-decllogic-function-declaxiom-decllogic-type-decl::=type logic-typelogic-type::=|ididlogic-const-decl::=logic type-exprlogic-function-decl::=logic type-exprpoly-id parameterslogic-predicate-decl::=::=};type-var-binderspolymorphic type;poly-id;predicatepoly-idaxiom-decl{ logic-decl ∗parameters ?axiom poly-id: pred;;Figure 2.14: Grammar for axiomatic declarations1234567/*@ inductive is_gcd(integer a, integer b, integer d) {@ case gcd_zero:@\forall integer n; is_gcd(n,0,n);@ case gcd_succ:@ \forall integer a,b,d; is_gcd(b, a % b, d) ==> is_gcd(a,b,d);@ }@*/This definition uses definite Horn clauses, hence is consistent.Example 2.22 already introduced an inductive definition of reachability in linked-lists, andwas also bases on definite Horn clauses thus consistent.2.6.4Axiomatic definitionsInstead of an explicit definition, one may introduce an axiomatic definitions for a set of types,predicates and logic functions, which amounts to declare the expected profiles and a set ofaxioms.
The grammar for those constructions is given on Figure 2.14.Example 2.40 The following axiomatization introduce a theory of finite lists of integers ala LISP.12345/*@ axiomatic IntList {@ type int_list;@ logic int_list nil;@ logic int_list cons(integer n,int_list l);@ logic int_list append(int_list l1,int_list l2);502.6.
LOGIC SPECIFICATIONS@ axiom append_nil:@\forall int_list l; append(nil,l) == l;@ axiom append_cons:@\forall integer n, int_list l1,l2;@append(cons(n,l1),l2) == cons(n,append(l1,l2));@ }@*/6789101112Like inductive definitions, there is no syntactic conditions which would guarantee axiomaticdefinitions to be consistent. It is usually up to the user to ensure that the introduction ofaxioms does not lead to a logical inconsistency.Example 2.41 The following axiomatization123456/*@ axiomatic sign {@logic integer get_sign(real x);@ axiom sign_pos: \forall real x; x >= 0. ==> get_sign(x) == 1;@ axiom sign_neg: \forall real x; x <= 0.
==> get_sign(x) == -1;@ }@*/is inconsistent since it implies sign(0.0) == 1 and sign(0.0) == -1, hence -1 == 12.6.5Polymorphic logic typesExperimentalWe consider here an algebraic specification setting based on multi-sorted logic, where typescan be polymorphic that is parametrized by other types. For example, one may declare thetype of polymorphic lists as1//@ type list<A>;One can then consider for instance list of integers (list <integer>), list of pointers (e.g.list <char*>), list of list of reals (list<list <real> >2 ), etc.The grammar of Figure 2.12 contains rules for declaring polymorphic types and using polymorphic type expressions.2.6.6Recursive logic definitionsExplicit definitions of logic functions and predicates can be recursive.
Declarations in thesame bunch of logic declarations are implicitly mutually recursive, so that mutually recursivefunctions are possible too.Example 2.42 The following logic declaration1234/*@ logic integer max_index{L}(int t[],integer n) =@ (n==0) ? 0 :@ (t[n-1]==0) ? n : max_index(t, n-1);@*/2In this latter case, note that the two ’>’ must be separated by a space, to avoid confusion with the shiftoperator.51CHAPTER 2. SPECIFICATION LANGUAGEtermext-quantifier::=|\lambda binders ; termext-quantifier ( term , term::=|\max | \min | \sum\product | \numofabstraction, term)Figure 2.15: Grammar for higher-order constructsdefines a logic function which returns the maximal index i between 0 and n-1 such that t[i]=0.There is no syntactic condition on such recursive definitions, such as limitation to primitive recursion.
In essence, a recursive definition of the form f(args) = e; where f occurs in expression e is just a shortcut for an axiomatic declaration of f with an axiom\forall args; f(args) = e. In other words, recursive definitions are not guaranteed to beconsistent, in the same way that axiomatics may introduce inconsistency. Of course, toolsmight provide a way to check consistency.2.6.7Higher-order logic constructionsExperimentalFigure 2.15 introduces new term constructs for higher-order logic.Abstraction The term \lambda τ1 x1 ,.
. .,τn xn ; t denotes the n-ary logic function whichmaps x1 , . . . ,xn to t. It has the same precedence as \forall and \existsExtended quantifiers Terms \quant(t1 ,t2 ,t3 ) where quant is max, min, sum, product ornumof are extended quantifications. t1 and t2 must have type integer , and t3 mustbe a unary function with an integer argument, and a numeric value (integer or real)except for \numof for which it should have a boolean value. Their meanings are given\max(i,j,f) = max{f ( i ), f ( i+1), . . . , f ( j )}\min(i,j,f) = min{f ( i ), f ( i+1), . . . , f ( j )}\sum(i,j,f) = f ( i ) + f ( i+1) + · · · + f ( j )as follows:\product(i,j,f) = f ( i ) × f ( i+1) × · · · × f ( j )\numof(i,j,f) = #{k | i ≤ k ≤ j ∧ f (k)}= \sum(i,j,\lambda integer k ; f(k) ? 1 : 0)If i>j then \sum and \numof above are 0, \product is 1, and \max and \min are unspecified(see Section 2.2.2).Example 2.43 Function that sums the element of an array of doubles.1234567891011/*@ requires n >= 0 && \valid(t+(0..n-1)) ;@ ensures \result == \sum(0,n-1,\lambda integer k; t[k]);@*/double array_sum(double t[],int n) {int i;double s = 0.0;/*@ loop invariant 0 <= i <= n;@ loop invariant s == \sum(0,i-1,\lambda integer k; t[k]);@ loop variant n-i;*/for (i=0; i < n; i++) s += t[i];522.6.
LOGIC SPECIFICATIONSlogic-def::=type logic-type =logic-type-def ;logic-type-def::=|record-type | sum-typetype-expr::={ type-expr id( ; type-expr id)∗record-typesum-type::=|? constructor( | constructor)∗constructor::=|ididtype-exprterm::=::=||||;?type abbreviation}constant constructor( type-expr(, type-expr)∗)non-constant constructor( type-expr(, type-expr)+)product typeterm. idrecord field access\match term{ match-cases }( term (, term)+ ){ (. id = term ;)+ }\let ( id (, id)+ ) =term ; termmatch-cases::=match-case +match-case::=case patpat::=||||||idid ( pat ( , pat)∗pat | patpattern-matchingtuplesrecords: term)_literal | { (. id = pat)∗( pat ( , pat )∗ )pat as id}constant constructornon-constant constructoror patternany patternrecord patterntuple patternpattern bindingFigure 2.16: Grammar for concrete logic types and pattern-matching1213}2.6.8return s;Concrete logic typesExperimentalLogic types may not only be declared but also be given a definition. Defined logic types canbe either record types, or sum types.
These definitions may be recursive. For record types,the field access notation t.id can be used, and for sum types, a pattern-matching constructionis available. Grammar rules for these additional constructions are given in Figure 2.1653CHAPTER 2. SPECIFICATION LANGUAGEpoly-idlabel-binders::=|||::=idid type-var-bindersid label-bindersid label-binderstype-var-binders{ id(, id)∗normal identifieridentifier for polymorphic objectnormal identifier with labelspolymorphic identifier with labels}Figure 2.17: Grammar for logic declarations with labelsExample 2.44 The declaration1//@ type list<A> = Nil | Cons(A,list<A>);introduces a concrete definition of finite lists.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
