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

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

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

. . . . . . . . . . . .INDEXIndex?, 16, 17_, 54abrupt clause, 67\allocable , 58, 61allocates , 60, 68allocation, 60\allocation , 58, 60allocation_status, 60annotation, 36loop, 36as, 54assert , 37assertion, 36assigns , 29, 30, 38, 45, 68, 69assumes, 29\at , 42, 43\automatic, 60axiom, 51axiomatic , 51\base_addr, 58behavior , 29, 31, 45, 87behaviors , 29\block_length , 28, 58, 59boolean, 18, 20breaks , 67case , 50, 54cast, 20–23complete, 29complete behaviors, 33comprehension, 35\concat, 65\Cons, 65continues , 67contract, 29, 36, 44, 87\dangling , 79data invariant, 70deallocation, 60decreases , 29, 46dependency, 69disjoint , 29disjoint behaviors, 34do, 38\dynamic, 60dynamic allocation, 60else , 76\empty, 34, 35ensures , 29, 30, 45, 67\eq_double, 23\eq_float , 23\exists , 17\exit_status , 67, 68exits, 67\false , 16, 17, 20for , 29, 37, 38, 40, 45\forall , 17formal parameter, 30, 31, 43, 71\freeable , 58, 61frees , 60, 68\fresh , 58, 61\from, 69function behavior, 31, 87function contract, 29, 87functional expression, 69\ge_double, 23\ge_float , 23ghost , 74, 76global , 70global invariant, 70grammar entriesC-compound-statement, 37C-external-declaration, 49C-statement, 37abrupt-clause-stmt, 67abrupt-clause, 67allocation-clause, 60assertion, 37, 40assigns-clause, 29, 69109INDEXassumes-clause, 29axiom-decl, 51axiomatic-decl, 51behavior-body-stmt, 45behavior-body, 29bin-op, 16binders, 18binder, 18breaks-clause, 67built-in-logic-type, 18completeness-clause, 29constructor, 54continues-clause, 67data-inv-decl, 70data-invariant, 70declaration, 70, 73, 76, 78decreases-clause, 29direct-declarator, 76dyn-allocation-addresses, 60ensures-clause, 29exits-clause, 67ext-quantifier, 53function-contract, 29ghost-selection-statement, 76ghost-type-specifier, 76ident, 17, 55indcase, 50inductive-def, 50inv-strength, 70label-binders, 55label-id, 43lemma-decl, 49literal, 16location-addresses, 58location-address, 58, 80locations, 29location, 29logic-const-decl, 51logic-const-def, 49logic-decl, 51logic-def, 49–51, 54logic-function-decl, 51, 57logic-function-def, 49, 57logic-predicate-decl, 51, 57logic-predicate-def, 49, 57logic-type-decl, 51logic-type-def, 54logic-type-expr, 18logic-type, 51loop-allocation, 60loop-annot, 38loop-assigns, 38loop-behavior, 38loop-clause, 38loop-invariant, 38loop-variant, 38match-cases, 54match-case, 54named-behavior-stmt, 45named-behavior, 29one-label, 58parameters, 49parameter, 49pat, 54poly-id, 16, 49postfix-expression, 76pred, 17, 29, 35, 43, 58, 80reads-clause, 57record-type, 54rel-op, 17requires-clause, 29returns-clause, 67simple-clause-stmt, 45simple-clause, 29statement-contract, 45statements-ghost, 76statement, 38, 45, 76struct-declaration, 76sum-type, 54terminates-clause, 29term, 16, 29, 43, 53, 54, 58, 66, 67tset, 35two-labels, 58type-expr, 18, 49, 54type-invariant, 70type-var-binders, 49type-var, 49unary-op, 16variable-ident, 18\gt_double, 23\gt_float , 23Here, 42, 43, 67hybridfunction, 55predicate, 55if , 76inductive , 50110INDEXinductive definitions, 50inductive predicates, 50Init, 42, 43\initialized , 79integer , 18, 20\inter , 35invariant, 40data, 70global, 70loop, 37strong, 70type, 70weak, 70invariant , 38, 40, 70\is_finite , 24\is_infinite , 24\is_minus_infinity , 24\is_NaN, 24\is_plus_infinity , 24l-value, 34\lambda, 53\le_double , 23\le_float , 23left-value, 87lemma, 49\length , 65\let , 16, 17, 54library, 58\list , 65location, 34, 64logic , 49, 51, 57logic specification, 48loopallocation, 63annotation, 36assigns, 37behavior, 38deallocation, 63invariant, 37variant, 39loop , 38, 60LoopCurrent, 42, 43LoopEntry, 42, 43\lt_double , 23\lt_float , 23lvalue, 87\match, 54\max, 53\min, 53model, 73module, 57\ne_double, 23\ne_float , 23\Nil , 65\nothing , 29\nth, 65\null , 58, 59\numof, 53\offset , 58, 59Old, 42, 43, 67\old , 29, 30, 42, 67, 68polymorphism, 52Post, 42, 43, 67post-state, 87Pre, 42, 43, 67pre-state, 87predicate, 16predicate , 49, 51, 57\product , 53pure expression, 87reads , 57, 78real , 18, 20real_of_double, 23real_of_float, 23recursion, 52\register , 60\repeat , 65requires , 29, 30\result , 29, 30, 67returns , 67\round_double, 23\round_float , 23\separated , 58–60set type, 64\sign , 24sizeof , 16, 22specification, 48statement contract, 36, 44\static , 60strong , 70\subset , 35\sum, 53term, 16111INDEXterminates , 29, 48termination, 39, 45\true , 16, 17, 20typeconcrete, 54polymorphic, 52record, 54sum, 54type , 51, 54, 70type invariant, 70\unallocated , 60\union, 35\valid , 58, 59valid_function, 80\valid_function , 80\valid_read , 58, 59variant , 38, 39, 46volatile , 78weak, 70while , 38\with , 16writes, 78112.

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

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