ACSL Language Reference (811287), страница 10

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 10)

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.16 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.44 Function that sums the elements of an array of doubles.12345678910111213/*@ 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];return s;}53CHAPTER 2.

SPECIFICATION LANGUAGElogic-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.17: Grammar for concrete logic types and pattern-matching2.6.8Concrete 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.17Example 2.45 The declaration1//@ type list<A> = Nil | Cons(A,list<A>);542.6. LOGIC SPECIFICATIONSidentlabel-binders::=::=idlabel-binders{ label-id(,normal identifier with labelslabel-id)∗}Figure 2.18: Grammar for logic declarations with labelsintroduces a concrete definition of finite lists. The logic definition123456/*@ logic integer list_length<A>(list<A> l) =@\match l {@case Nil : 0@case Cons(h,t) : 1+list_length(t)@};@*/defines the length of a list by recursion and pattern-matching.2.6.9Hybrid functions and predicatesLogic functions and predicates may take arguments with either (pure) C type or logic type.Such a predicate (or function) can either be defined with the same syntax as before (oraxiomatized).

However, such definitions usually depends on one or more program points,because it depends upon memory states, via expressions such as:• pointer dereferencing: *p, p->f;• array access: t[i];• address-of operator: &x;• built-in predicate depending on memory: \validTo make such a definition safe, it is mandatory to add after the declared identifier a setof labels, between curly braces.

We then speak of a hybrid predicate (or function). Thegrammar for identifier is extended as shown on Figure 2.18. Expressions as above must thenbe enclosed into the \at construct to refer to a given label. However, to ease reading of suchlogic expressions, it is allowed to omit a label whenever there is only one label in the context.Example 2.46 The following annotations declare a function which returns the number ofoccurrences of a given double in a memory block storing doubles between the given indexes,together with the related axioms. It should be noted that without labels, this axiomatizationwould be inconsistent, since the function would not depend on the values stored in t, hencethe two last axioms would say both that a==b+1 and a==b for some a and b.12345678910/*@ axiomatic NbOcc {@ // nb_occ(t,i,j,e) gives the number of occurrences of e in t[i..j]@ // (in a given memory state labelled L)@ logic integer nb_occ{L}(double *t, integer i, integer j,@double e);@ axiom nb_occ_empty{L}:@\forall double *t, e, integer i, j;@i > j ==> nb_occ(t,i,j,e) == 0;@ axiom nb_occ_true{L}:@\forall double *t, e, integer i, j;55CHAPTER 2.

SPECIFICATION LANGUAGE@i <= j && t[j] == e ==>@nb_occ(t,i,j,e) == nb_occ(t,i,j-1,e) + 1;@ axiom nb_occ_false{L}:@\forall double *t, e, integer i, j;@i <= j && t[j] != e ==>@nb_occ(t,i,j,e) == nb_occ(t,i,j-1,e);@ }@*/1112131415161718Example 2.47 This second example defines a predicate that indicates whether two memoryblocks of the same size are a permutation of each other. It illustrates the use of more than asingle label. Thus, the \at operator is mandatory here.

Indeed the two blocks may come fromtwo distinct memory states. Typically, one of the post conditions of a sorting function wouldbe permut{Pre,Post}(t,t).12345678910111213141516171819202122/*@ axiomatic Permut {@ // permut{L1,L2}(t1,t2,n) is true whenever t1[0..n-1] in state L1@ // is a permutation of t2[0..n-1] in state L2@ predicate permut{L1,L2}(double *t1, double *t2, integer n);@ axiom permut_refl{L}:@\forall double *t, integer n; permut{L,L}(t,t,n);@ axiom permut_sym{L1,L2} :@\forall double *t1, *t2, integer n;@permut{L1,L2}(t1,t2,n) ==> permut{L2,L1}(t2,t1,n) ;@ axiom permut_trans{L1,L2,L3} :@\forall double *t1, *t2, *t3, integer n;@permut{L1,L2}(t1,t2,n) && permut{L2,L3}(t2,t3,n)@==> permut{L1,L3}(t1,t3,n) ;@ axiom permut_exchange{L1,L2} :@\forall double *t1, *t2, integer i, j, n;@\at(t1[i],L1) == \at(t2[j],L2) &&@\at(t1[j],L1) == \at(t2[i],L2) &&@( \forall integer k; 0 <= k < n && k != i && k != j ==>@\at(t1[k],L1) == \at(t2[k],L2))@==> permut{L1,L2}(t1,t2,n);@ }@*/2.6.10Memory footprint specification: reads clauseExperimentalLogic declarations can be augmented with a reads clause, with the syntax given in Figure 2.19,which extends the one of Figure 2.13.

This feature allows to specify the footprint of a hybridpredicate or function, that is, the set of memory locations that it depends on. From suchinformation, one might deduce properties of the form f {L1 }(args) = f {L2 }(args) if it isknown that between states L1 and L2 , the memory changes are disjoint from the declaredfootprint.Example 2.48 The following is the same as example 2.46 augmented with a reads clause.123/*@ axiomatic Nb_occ {@ logic integer nb_occ{L}(double *t, integer i, integer j,@double e)562.6.

LOGIC SPECIFICATIONSlogic-function-decllogic-predicate-decl::=::=logic type-expr poly-idparameters reads-clausepredicate poly-idparameters ? reads-clausereads-clause::=reads locationslogic-function-def::=logic type-expr poly-idparameters reads-clauselogic-predicate-def::=predicate poly-idparameters ? reads-clause;;= term= pred;;Figure 2.19: Grammar for logic declarations with reads clauses@reads t[i..j];@@ axiom nb_occ_empty{L}: // ...@@ // ...@ }@*/45678910If for example a piece of code between labels L_1 and L_2 only modifies t[k] for some index koutside i..j, then one can deduce that nb_occ{L_1}(t,i,j,e)==nb_occ{L_2}(t,i,j,e).2.6.11Specification ModulesExperimentalSpecification modules can be provided to encapsulate several logic definitions, for example123456789101112131415161718192021/*@ module List {@@ type list<A> = Nil | Cons(A , list<A>);@@logic integer length<A>(list<A> l) =@\match l {@case Nil : 0@case Cons(h,t) : 1+length(t) } ;@@logic A fold_right<A,B>((A -> B -> B) f, list<A> l, B acc) =@\match l {@case Nil : acc@case Cons(h,t) : f(h,fold_right(f,t,acc)) } ;@@logic list<A> filter<A>((A -> boolean) f, list<A> l) =@fold_right((\lambda A x, list<A> acc;@f(x) ? Cons(x,acc) : acc), Nil) ;@@ }@*/Module components are then accessible using a qualified notation like List::length.57CHAPTER 2.

Характеристики

Список файлов книги