ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (1184405), страница 20
Текст из файла (страница 20)
New in Version 4.2.1 (April 2010)• added alternative specification of remove copy algorithm that uses ghost variables• added Chapter on heap operations• added mismatch algorithm• moved algorithms adjacent find and min element from the appendix to Chapter 3• added typedefs size_type and value_type and used them in all algorithms• renamed is_valid_int_range as is_valid_rangeA.5. New in Version 4.2.0 (January 2010)• complete rewrite of previous release• adaption to Frama-C Beryllium 2 releaseA.6. Unofficial Release as part of the ES PASS project (March2009)144Bibliography[1] ANSI/ISO C Specification Language. http://frama-c.com/acsl.html.[2] Jessie Plug-in.
http://frama-c.com/jessie.html.[3] Frama-C Software Analyzers. http://frama-c.com.[4] CEA LIST, Laboratory of Applied Research on Software-Intensive Technologies. http://www-list.cea.fr/gb/index_gb.htm.[5] INRIA-Saclay, French National Institute for Research in Computer Science and Control .http://www.inria.fr/saclay/.[6] LRI, Laboratory for Computer Science at Université Paris-Sud. http://www.lri.fr/.[7] Why – Software Verification Platform. http://why.lri.fr.[8] Fraunhofer Institut Rechnerarchitektur und Softwaretechnik (FIRST).first.fraunhofer.de.[9] Virgile Prevosto.ACSL Mini-Tutorial.acsl-tutorial.pdf.http://www.http://frama-c.com/download/[10] Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, BenjaminMonate, Yannick Moy, and Virgile Prevosto.
ANSI/ISO C Specification Language,Version 1.4 Frama-C Boron implementation. http://frama-c.com/download/acsl-implementation-Boron-20100401.pdf, April 2010.[11] Standard Template Library Programmer’s Guide. http://www.sgi.com/tech/stl,2010.[12] Programming languages – C, Committee Draft. http://www.open-std.org/JTC1/SC22/WG14/www/docs/n1362.pdf, 2009.[13] Claude Marché and Yannick Moy. Jessie Plugin Tutorial, Beryllium Version. http://frama-c.com/jessie/jessie-tutorial.pdf, 2010.[14] C.A.R.
Hoare. An axiomatic basis for computer programming. Communications of the ACM,12:576–583, 1969.[15] Robert W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Proc. Symposium on Applied Mathematics, volume 19 of Mathematical Aspects of Computer Science,pages 19–32, Providence, RI, 1967.
American Mathematical Society.[16] Richard Fitzpatrick, editor. Euklid’s Elements of Geometry. Austin/TX, 2008.[17] David Hilbert. Grundlagen der Geometrie. B.G.Teubner, Stuttgart, 1968.145[18] Martin Odersky, Lex Spoon, and Bill Venners. Programming in Scala. Artima, 2008.[19] Sylvain Conchon, Evelyne Contejean, and Johannes Kanig. Homepage of the Alt-Ergo Theorem Prover. http://alt-ergo.lri.fr/.[20] Clark Barrett and Cesare Tinelli. Homepage of CVC3. http://www.cs.nyu.edu/acsys/cvc3/, 2010.[21] Homepage of the Simplify Theorem Prover. http://freshmeat.net/projects/simplifyprover/, 2007.[22] Microsoft Research.Homepage of the Z3 SMT Solver.microsoft.com/en-us/um/redmond/projects/z3/.146http://research..