ACSL Language Reference (811287), страница 9
Текст из файла (страница 9)
We call cluster a set of mutually recursive functionswhich is a strongly connected component of the call graph. Within each cluster, each functionmust be annotated with a decreases clause with the same relation R (syntactically). Then,in the body of any function f of that cluster, any recursive call to a function g must occurin a state where the measure attached to g is smaller (w.r.t R) than the measure of f in thepre-state of f. This also applies when g is f itself.Example 2.35 Here are the classical factorial and Fibonacci functions:12345678/*@ requires n <= 12;@ decreases n;@*/int fact(int n) {if (n <= 1) return 1;return n * fact(n-1);}91011121314//@ decreases n;int fib(int n) {if (n <= 1) return 1;return fib(n-1) + fib(n-2);}Example 2.36 This example illustrates mutual recursion:12345678/*@requires n>=0;decreases n;*/int even(int n) {if (n == 0) return 1;return odd(n-1);}947CHAPTER 2. SPECIFICATION LANGUAGE1011121314151617/*@requires x>=0;decreases x;*/int odd(int x) {if (x == 0) return 0;return even(x-1);}2.5.4Non-terminating functionsExperimentalThere are cases where a function is not supposed to terminate.
For instance, the main functionof a reactive program might be a while (1) which indefinitely waits for an event to process.More generally, a function can be expected to terminate only if some preconditions are met.In those cases, a terminates clause can be added to the contract of the function, under thefollowing form://@ terminates p;The semantics of such a clause is as follows: if p holds, then the function is guaranteed toterminate (more precisely, its termination must be proved).
If such a clause is not present(and in particular if there is no function contract at all), it defaults to terminates \true;that is the function is supposed to always terminate, which is the expected behavior of mostfunctions.Note that nothing is specified for the case where p does not hold: the function may terminateor not. In particular, terminates \false ; does not imply that the function loops forever. Apossible specification for a function that never terminates is the following:1234/*@ ensures \false ;terminates \false ;*/void f() { while(1); }Example 2.37 A concrete example of a function that may not always terminate is theincr_list function of example 2.23. In fact, The following contract is also acceptable forthis function:123456782.6// this time, the specification accepts circular lists, but does not ensure// that the function terminates on them (as a matter of fact, it does not)./*@ terminates reachable(p,\null);@ assigns { q->hd | struct list *q ; reachable(p,q) } ;@*/void incr_list(struct list *p) {while (p) { p->hd++ ; p = p->next; }}Logic specificationsThe language of logic expressions used in annotations can be extended by declarations of newlogic types, and new constants, logic functions and predicates.
These declarations follow the482.6. LOGIC SPECIFICATIONSC-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::=*/type variable>< type-var(, type-var)∗>poly-id::=identlogic-const-def::=logic type-exprpoly-id = termlogic-function-def::=polymorphic typetype-var-binders;logic type-exprpoly-id parametersterm ;logic-predicate-def::=::==predicatepoly-id parameters ?pred ;parameterspolymorphic object identifier=( parameter(, parameter)∗parameter::=type-exprlemma-decl::=lemma poly-idpred ;)id:Figure 2.13: Grammar for global logic definitionsclassical setting of algebraic specifications.
The grammar for these declarations is given inFigure 2.13.2.6.1Predicate and function definitionsNew functions and predicates can be defined by explicit expressions, given after an equalsign.Example 2.38 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);@*/illustrates the definition of a new predicate is_positive with an integer parameter, and a newlogic function sign with a real parameter returning an integer.49CHAPTER 2. SPECIFICATION LANGUAGElogic-def::=inductive-definductive-def::=inductivepoly-idindcase::=parameters ?case poly-id: pred{ indcase ∗};Figure 2.14: Grammar for inductive definitions2.6.2LemmasLemmas are user-given propositions, a facility that might help theorem provers to establishvalidity of ACSL specifications.Example 2.39 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.14.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.40 The following introduces a predicate isgcd(x,y,d) meaning that d is thegreatest common divisor of x and y.502.6. LOGIC SPECIFICATIONSlogic-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.15: 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.23 already introduced an inductive definition of reachability in linked-lists, andwas also based on definite Horn clauses, and is 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.15.Example 2.41 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);51CHAPTER 2. SPECIFICATION LANGUAGE@ 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));@ }@*/6789101112Unlike inductive definitions, there is no syntactic condition that 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.42 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 typesWe 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.13 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.43 The following logic declaration1234/*@ logic integer max_index{L}(int t[],integer n) =@ (n==0) ? 0 :@ (t[n-1]==0) ? n-1 : max_index(t, n-1);@*/defines a logic function which returns the maximal index i between 0 and n-1 such that t[i]=0.2In this latter case, note that the two ’>’ must be separated by a space, to avoid confusion with the shiftoperator.522.6. LOGIC SPECIFICATIONStermext-quantifier::=|\lambda binders ; termext-quantifier ( term , term::=|\max | \min | \sum\product | \numofabstraction, term)Figure 2.16: Grammar for higher-order constructsThere is no syntactic condition on such recursive definitions, such as limitation to primitive recursion.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
