ACSL Language Reference (811287), страница 19
Текст из файла (страница 19)
APPENDICESA.6.3Version 1.10• Change keyword for importing libraries (section 2.6.11)• Fix numerous typos reported by David Cok• Disallow meaningless assigns \nothing \from x (section 2.10)A.6.4Version 1.9• Fix typo in definition of \fresh predicate (section 2.7.3)• Fix grammar inconsistencies– use proper C rules names– fix mismatch in non-terminal names• Rename "Unspecified values" to "Dangling pointers" and precise it (section 2.13.2)A.6.5Version 1.8• Mention binary literal constant typingA.6.6Version 1.7• Added missing shift operators in figure 2.1• Modified syntax for naming terms and predicates (figures 2.2 and 2.1)• Added syntax rule for literal constants (figure 2.1)A.6.7Version 1.6• Modified syntax for model fields (section 2.11.2)• Added missing logical xor operator (figure 2.1).• Addition of logical labels related to loops (section 2.4.3).• Addition of labels to built-ins related to memory blocks (section 2.7.1)• Introduction of \valid_read built-in and clarification of the notion of validity (section 2.7.1).• Introduction of built-in \allocable , \allocation , \freeable and \fresh (section 2.7.3).• Introduction of allocates and frees clauses (section 2.7.3).• Clarify the semantics of assigns clauses into statement contract.• Improvements to the volatile clause (section 2.12.1).• Clarify the evaluation of arrays inside an at (section 2.4.3).102A.6.
CHANGESA.6.8Version 1.5• Clarify the status of loop invariant in presence of break or side-effects in the loop test.• Introduction of \with keyword for functional updates.• Added bnf entry for completeness of function behaviors.• Order of clauses in statement contracts is now fixed.• requires clauses are allowed before behaviors of statement contracts.• Added explicit singleton construct for sets.• Introduction of logical arrays.• Operations over pointers and arrays have been precised.• Predicate \initialized (section 2.13.1) now takes a set of pointers as argument.A.6.9Version 1.4• Added UTF-8 counterparts for built-in types ( integer , real , boolean).• Fixed typos in the examples corresponding to features implemented in Frama-C.• Order of clauses in function contracts is now fixed.• Introduction of abrupt termination clauses.• Introduction of axiomatic to gather predicates, logic functions, and their defining axioms.• Added specification templates appendix for common specification issues.• Use of sets as first-class term has been precised.• Fixed semantics of predicate \separated .A.6.10Version 1.3• Functional update of structures.• Terminates clause in function behaviors.• Typos reported by David Mentré.A.6.11Version 1.2This is the first public release of this document.103BIBLIOGRAPHYBibliography[1] Jean-Raymond Abrial.
The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.[2] Ali Ayad and Claude Marché. Behavioral properties of floating-point programs. Hisseopublications, 2009. http://hisseo.saclay.inria.fr/ayad09.pdf.[3] Sylvie Boldo and Jean-Christophe Filliâtre. Formal Verification of Floating-Point Programs. In 18th IEEE International Symposium on Computer Arithmetic, pages 187–194,Montpellier, France, June 2007.[4] Patrice Chalin. Reassessing JML’s logical foundation. In Proceedings of the 7th Workshopon Formal Techniques for Java-like Programs (FTfJP’05), Glasgow, Scotland, July 2005.[5] Patrice Chalin.
A sound assertion semantics for the dependable systems evolution verifying compiler. In Proceedings of the International Conference on Software Engineering(ICSE’07), pages 23–33, Los Alamitos, CA, USA, 2007. IEEE Computer Society.[6] David R. Cok and Joseph R.
Kiniry. ESC/Java2 implementation notes. Technical report,University College Dublin, May 2007. http://secure.ucd.ie/products/opensource/ESCJava2/ESCTools/docs/Escjava2-ImplementationNotes.pdf.[7] Jeremy Condit, Matthew Harren, Scott McPeak, George C. Necula, and Westley Weimer.Ccured in the real world. In PLDI ’03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, pages 232–244, 2003.[8] Jeremy Paul Condit, Matthew Thomas Harren, Zachary Ryan Anderson, David Gay, andGeorge Necula. Dependent types for low-level programming. In ESOP ’07: Proceedingsof the 16th European Symposium on Programming, October 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] 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.105BIBLIOGRAPHY[12] International Organization for Standardization (ISO).
The ANSI C standard (C99).http://www.open-std.org/JTC1/SC22/WG14/www/docs/n1124.pdf.[13] Brian Kernighan and Dennis Ritchie. The C Programming Language (2nd Ed.). PrenticeHall, 1988.[14] Joseph Kiniry. ESC/Java2. http://kind.ucd.ie/products/opensource/ESCJava2/.[15] Gary Leavens. Jml. http://www.eecs.ucf.edu/~leavens/JML/.[16] 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.[17] 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.[18] 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.[19] 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.[20] Yannick Moy.
Union and cast in deductive verification. Technical Report ICIS-R07015,Radboud University Nijmegen, July 2007. http://www.lri.fr/~moy/union_and_cast/union_and_cast.pdf.[21] 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.[22] Arun D. Raghavan and Gary T. Leavens. Desugaring JML method specifications. Technical Report 00-03a, Iowa State University, 2000.[23] David Stevenson et al. An american national standard: IEEE standard for binary floatingpoint arithmetic. ACM SIGPLAN Notices, 22(2):9–25, 1987.[24] Wikipedia. First order logic. http://en.wikipedia.org/wiki/First_order_logic.[25] Wikipedia. IEEE 754. http://en.wikipedia.org/wiki/IEEE_754-1985.106LIST 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 . . . . . . . . . . . . . . . . . . . . . .
. . . . . . .352.8Grammar for assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .372.9Grammar for loop annotations . . . . . . . . . . . . . . . . . . . . . . . . . .382.10 Grammar for general inductive invariants . . . . . . . . . .
. . . . . . . . . .402.11 Grammar for at construct . . . . . . . . . . . . . . . . . . . . . . . . . . . . .432.12 Grammar for statement contracts . . . . . . . . . . . . . . . . . . . . . . . . .452.13 Grammar for global logic definitions . . . . . . . . . . . . . . . . . . . . . . .492.14 Grammar for inductive definitions .
. . . . . . . . . . . . . . . . . . . . . . .502.15 Grammar for axiomatic declarations . . . . . . . . . . . . . . . . . . . . . . .512.16 Grammar for higher-order constructs . . . . . . . . . . . . . . . . . . . . . . .532.17 Grammar for concrete logic types and pattern-matching . . . . . . . . . . . .542.18 Grammar for logic declarations with labels . . . . . . . . . . . . . . . . . . .
.552.19 Grammar for logic declarations with reads clauses . . . . . . . . . . . . . . . .572.20 Grammar extension of terms and predicates about memory . . . . . . . . . .582.21 Grammar for dynamic allocations and deallocations . . . . . . . . . . . . . .602.22 Notations for built-in list datatype . . . . . .
. . . . . . . . . . . . . . . . . .662.23 Grammar of contracts about abrupt terminations . . . . . . . . . . . . . . . .672.24 Grammar for dependencies information. . . . . . . . . . . . . . . . . . . . .692.25 Grammar for declarations of data invariants . . . . . . . . . . . . . . . .
. . .702.26 Grammar for declarations of model variables and fields . . . . . . . . . . . . .732.27 Grammar for ghost statements . . . . . . . . . . . . . . . . . . . . . . . . . .762.28 Grammar for volatile constructs . . . . . . . . . . . . . . . . . . . . . . . . . .782.29 Grammar for predicates related to well-typedness80107. . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
