ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver (1185160), страница 18
Текст из файла (страница 18)
Dependent types for low-level programming. In ESOP ’07: Proceedingsof the 16th European Symposium on Programming, Oct 2006.[9] Jean-Christophe Filliâtre and Claude Marché. Multi-prover verification of C programs.In Jim Davies, Wolfram Schulte, and Mike Barnett, editors, 6th International Conferenceon Formal Engineering Methods, volume 3308 of Lecture Notes in Computer Science,pages 15–29, Seattle, WA, USA, November 2004.
Springer.[10] Jean-Christophe Filliâtre and Claude Marché. The Why/Krakatoa/Caduceus platformfor deductive program verification. In Werner Damm and Holger Hermanns, editors, 19thInternational Conference on Computer Aided Verification, Lecture Notes in ComputerScience, Berlin, Germany, July 2007. Springer.[11] The Frama-C framework for analysis of C code. http://frama-c.cea.fr/.[12] A. Giorgetti and J. Groslambert. JAG: JML Annotation Generation for verifying temporal properties. In FASE’2006, Fundamental Approaches to Software Engineering, volume3922 of LNCS, pages 373–376, Vienna, Austria, March 2006. Springer.103BIBLIOGRAPHY[13] International Organization for Standardization (ISO).
The ANSI C standard (C99).http://www.open-std.org/JTC1/SC22/WG14/www/docs/n1124.pdf.[14] Brian Kernighan and Dennis Ritchie. The C Programming Language (2nd Ed.). PrenticeHall, 1988.[15] Joseph Kiniry. ESC/Java2. http://kind.ucd.ie/products/opensource/ESCJava2/.[16] Gary Leavens. Jml.
http://www.eecs.ucf.edu/~leavens/JML/.[17] Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary design of JML: Abehavioral interface specification language for Java. Technical Report 98-06i, Iowa StateUniversity, 2000.[18] Gary T. Leavens, K. Rustan M. Leino, and Peter Müller. Specification and verificationchallenges for sequential object-oriented programs. Form. Asp. Comput., 19(2):159–189,2007.[19] Gary T. Leavens, K.
Rustan M. Leino, Erik Poll, Clyde Ruby, and Bart Jacobs. JML:notations and tools supporting detailed design in Java. In OOPSLA 2000 Companion,Minneapolis, Minnesota, pages 105–106, 2000.[20] Claude Marché. Towards modular algebraic specifications for pointer programs: a casestudy. In H.
Comon-Lundh, C. Kirchner, and H. Kirchner, editors, Rewriting, Computation and Proof, volume 4600 of Lecture Notes in Computer Science, pages 235–258.Springer-Verlag, 2007.[21] Yannick Moy. Union and cast in deductive verification. Technical Report ICIS-R07015,Radboud University Nijmegen, jul 2007. http://www.lri.fr/~moy/union_and_cast/union_and_cast.pdf.[22] George C. Necula, Scott McPeak, and Westley Weimer.
CCured: Type-safe retrofittingof legacy code. In Symposium on Principles of Programming Languages, pages 128–139,2002.[23] Arun D. Raghavan and Gary T. Leavens. Desugaring JML method specifications. Technical Report 00-03a, Iowa State University, 2000.[24] David Stevenson et al. An american national standard: IEEE standard for binary floatingpoint arithmetic. ACM SIGPLAN Notices, 22(2):9–25, 1987.[25] Wikipedia. First order logic. http://en.wikipedia.org/wiki/First_order_logic.[26] Wikipedia. IEEE 754. http://en.wikipedia.org/wiki/IEEE_754-1985.104LIST OF FIGURESList of Figures2.1Grammar of terms . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .162.2Grammar of predicates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .172.3Grammar of binders and type expressions . . . . . . . . . . . . . . . . . . . .182.4Operator precedence . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . .192.5Grammar of function contracts . . . . . . . . . . . . . . . . . . . . . . . . . .292.6\old and \result in terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .292.7Grammar for sets of terms . . . .
. . . . . . . . . . . . . . . . . . . . . . . . .342.8Grammar for assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .362.9Grammar for loop annotations . . . . . . . . . . . . . . . . . . . . . . . . . .372.10 Grammar for general inductive invariants . . . . . . . . . . . . . . . . . . . .392.11 Grammar for statement contracts .
. . . . . . . . . . . . . . . . . . . . . . . .442.12 Grammar for global logic definitions . . . . . . . . . . . . . . . . . . . . . . .482.13 Grammar for inductive definitions . . . . . . . . . . . . . . . . . . . . . . . .492.14 Grammar for axiomatic declarations . . . . . . . . . . . . . . . . . . . . . . .502.15 Grammar for higher-order constructs . . .
. . . . . . . . . . . . . . . . . . . .522.16 Grammar for concrete logic types and pattern-matching . . . . . . . . . . . .532.17 Grammar for logic declarations with labels . . . . . . . . . . . . . . . . . . . .542.18 Grammar for logic declarations with reads clauses . . . . . . . . . .
. . . . . .562.19 Grammar extension of terms and predicates about memory . . . . . . . . . .572.20 Grammar for dynamic allocations and deallocations . . . . . . . . . . . . . .592.21 Grammar of contracts about abrupt terminations . . . . . . . . . . . . . . . .642.22 Grammar for dependencies information. . . . . . .
. . . . . . . . . . . . . .662.23 Grammar for declarations of data invariants . . . . . . . . . . . . . . . . . . .682.24 Grammar for declarations of model variables and fields . . . . . . . . . . . . .702.25 Grammar for ghost statements . . . . . . . . . . . .
. . . . . . . . . . . . . .732.26 Grammar for volatile constructs . . . . . . . . . . . . . . . . . . . . . . . . . .75105INDEXIndex?, 16, 17_, 53abrupt clause, 64\allocable , 57, 60allocates , 59, 66allocation, 59\allocation , 57, 60allocation_status, 59annotation, 36loop, 36as, 53assert , 36assertion, 36assigns , 29, 30, 37, 44, 66assumes, 29\at , 41\automatic, 59axiom, 50axiomatic , 50\base_addr, 57, 58behavior , 29, 31, 44, 85behaviors , 29\block_length , 28, 57, 58boolean, 18, 20breaks , 64, 65case , 49, 53cast, 20–23complete, 29complete behaviors, 33comprehension, 35continues , 64, 65contract, 28, 36, 43, 85\danling , 77data invariant, 67deallocation, 59decreases , 29, 45dependency, 66disjoint , 29disjoint behaviors, 33do, 37\dynamic, 59dynamic allocation, 59else , 73\empty, 34ensures , 29, 30, 44, 64\eq_double, 23\eq_float , 23\exists , 17\exit_status , 64, 65exits, 64\false , 16, 17, 20for , 29, 36, 37, 39, 44\forall , 17formal parameter, 29, 30, 42, 68\freeable , 57, 60frees , 59, 66\fresh , 57, 60\from, 66function behavior, 31, 85function contract, 28, 85functional expression, 66\ge_double, 23\ge_float , 23ghost , 72, 73global , 68global invariant, 67grammar entriesC-compound-statement, 36C-external-declaration, 48C-statement, 36abrupt-clause-fn, 64abrupt-clause-stmt, 64allocation-clause, 59assertion, 36, 39assigns-clause, 29, 66assumes-clause, 29axiom-decl, 50107INDEXaxiomatic-decl, 50behavior-body-stmt, 44behavior-body, 29bin-op, 16binders, 18binder, 18breaks-clause, 64built-in-logic-type, 18completeness-clause, 29constructor, 53continues-clause, 64data-inv-decl, 68data-invariant, 68declaration, 68, 70, 73, 75decreases-clause, 29direct-declarator, 73dyn-allocation-addresses, 59ensures-clause, 29exits-clause, 64ext-quantifier, 52function-contract, 29ghost-selection-statement, 73ghost-type-specifier, 73indcase, 49inductive-def, 49inv-strength, 68label-binders, 54lemma-decl, 48literal, 16location-addresses, 57location-address, 57locations, 29location, 29logic-const-decl, 50logic-const-def, 48logic-decl, 50logic-def, 48–50, 53logic-function-decl, 50, 56logic-function-def, 48, 56logic-predicate-decl, 50, 56logic-predicate-def, 48, 56logic-type-decl, 50logic-type-def, 53logic-type-expr, 18logic-type, 50loop-allocation, 59loop-annot, 37loop-assigns, 37loop-behavior, 37loop-clause, 37loop-invariant, 37loop-variant, 37match-cases, 53match-case, 53named-behavior-stmt, 44named-behavior, 29one-label, 57parameters, 48parameter, 48pat, 53poly-id, 48, 54postfix-expression, 73pred, 17, 29, 34, 57reads-clause, 56record-type, 53rel-op, 17requires-clause, 29returns-clause, 64simple-clause-stmt, 44simple-clause, 29statement-contract, 44statements-ghost, 73statement, 37, 44, 73struct-declaration, 73sum-type, 53terminates-clause, 29term, 16, 29, 52, 53, 57, 64tset, 34two-labels, 57type-expr, 18, 48, 53type-invariant, 68type-var-binders, 48type-var, 48unary-op, 16variable-ident, 18\gt_double, 23\gt_float , 23Here, 41, 65hybridfunction, 54predicate, 54if , 73inductive , 49inductive definitions, 49inductive predicates, 49\initialized , 76integer , 18, 20108INDEX\inter , 34invariant, 39data, 67global, 67loop, 37strong, 67type, 67weak, 67invariant , 37, 39, 68\is_finite , 24\is_NaN, 24l-value, 34\lambda, 52\le_double , 23\le_float , 23left-value, 85lemma, 48\let , 16, 17, 53library, 57location, 34, 63logic , 48, 50, 56logic specification, 47loopallocation, 62annotation, 36assigns, 37behavior, 38deallocation, 62invariant, 37variant, 39loop , 37, 59LoopCurrent, 41LoopEntry, 41\lt_double , 23\lt_float , 23lvalue, 85\match, 53\max, 52\min, 52model, 70module, 56\ne_double, 23\ne_float , 23\nothing , 29\null , 57, 58\numof, 52\offset , 57, 58Old, 41, 65\old , 29, 41, 65polymorphism, 51Post, 41, 65post-state, 85Pre, 41, 65pre-state, 85predicate, 16predicate , 48, 50, 56\product , 52pure expression, 85reads , 56, 75real , 18, 20real_of_double, 23real_of_float, 23recursion, 51\register , 59requires , 29, 30\result , 29, 65returns , 64, 65\round_double, 23\round_float , 23\separated , 57, 59set type, 63sizeof , 16, 22specification, 47statement contract, 36, 43\static , 59strong , 68\subset , 34\sum, 52term, 16terminates , 29, 47termination, 39, 44\true , 16, 17, 20typeconcrete, 53polymorphic, 51record, 53sum, 53type , 50, 53, 68type invariant, 67\unallocated , 59\union, 34\valid , 57, 58109INDEX\valid_read , 57, 58variant , 37, 39, 45volatile , 75weak, 68while , 37\with , 16writes, 75110.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
