ACSL Language Reference (811287)
Текст из файла
ACSL: ANSI/ISO C Specification LanguageVersion 1.12ACSL: ANSI/ISO C SpecificationLanguageVersion 1.12Patrick Baudin1 , Pascal Cuoq1 , Jean-Christophe Filliâtre4,3 , Claude Marché3,4 ,Benjamin Monate1 , Yannick Moy2,4,3 , Virgile Prevosto11234CEA LIST, Software Reliability Laboratory, Saclay, F-91191France Télécom, Lannion, F-22307INRIA Saclay - Île-de-France, ProVal, Orsay, F-91893LRI, Univ Paris-Sud, CNRS, Orsay, F-91405This work is licensed under a “CC BY 4.0” license.Sources are available at https://github.com/acsl/acsl.©2009-2016 CEA LIST and INRIAThis work has been supported by the ANR project CAT (ANR-05-RNTL-0030x), by theANR CIFRE contract 2005/973, by the ANR project U3CAT (08-SEGI-021-xx), and ANRPICF project DEVICE-Soft (2009-CARN-006-01).CONTENTSContents1 Introduction111.1Organization of this document .
. . . . . . . . . . . . . . . . . . . . . . . . .111.2Generalities about Annotations . . . . . . . . . . . . . . . . . . . . . . . . . .111.2.1Kinds of annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . .121.2.2Parsing annotations in practice . . . . . . . . . . . . . . . . . . . .
. .121.2.3About preprocessing . . . . . . . . . . . . . . . . . . . . . . . . . . . .131.2.4About keywords . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13Notations for grammars . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . .131.32 Specification language152.1Lexical rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .152.2Logic expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .162.2.1Operators precedence . . . . . . . .
. . . . . . . . . . . . . . . . . . .192.2.2Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .192.2.3Typing. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .202.2.4Integer arithmetic and machine integers . . . . . . . . . . . . . . . . .202.2.5Real numbers and floating point numbers . . . .
. . . . . . . . . . . .232.2.6C arrays and pointers . . . . . . . . . . . . . . . . . . . . . . . . . . .252.2.7Structures, Unions and Arrays in logic . . . . . . . . . . . . . . . . . .26Function contracts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .292.3.1Built-in constructs \old and \result .
. . . . . . . . . . . . . . . . . . .302.3.2Simple function contracts . . . . . . . . . . . . . . . . . . . . . . . . .302.3.3Contracts with named behaviors . . . . . . . . . . . . . . . . . . . . .312.3.4Memory locations and sets of terms . . . . . . . . . . . . . . . . . . .342.3.5Default contracts, multiple contracts . .
. . . . . . . . . . . . . . . . .36Statement annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .362.4.1Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .372.4.2Loop annotations . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . .372.4.3Built-in construct \at . . . . . . . . . . . . . . . . . . . . . . . . . . .422.32.45CONTENTS2.4.42.52.62.72.82.9Statement contracts . . . . . . . . . . . . . . . . . . . . . . . . . . . .44Termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . .452.5.1Integer measures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .462.5.2General measures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .462.5.3Recursive function calls . . . . . . . . . . . . . . . . . . . . . . . . .
.472.5.4Non-terminating functions . . . . . . . . . . . . . . . . . . . . . . . . .48Logic specifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .482.6.1Predicate and function definitions . . . . . . . . . . . . . . . . . . . .492.6.2Lemmas . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . .502.6.3Inductive predicates . . . . . . . . . . . . . . . . . . . . . . . . . . . .502.6.4Axiomatic definitions. . . . . . . . . . . . . . . . . . . . . . . . . . .512.6.5Polymorphic logic types . . . . . . . . . . . . . . . . . . . . . . .
. . .522.6.6Recursive logic definitions . . . . . . . . . . . . . . . . . . . . . . . . .522.6.7Higher-order logic constructions . . . . . . . . . . . . . . . . . . . . . .532.6.8Concrete logic types . . . . . . . . . . . . . . . . . . . . . . . . . . . .542.6.9Hybrid functions and predicates .
. . . . . . . . . . . . . . . . . . . .552.6.10 Memory footprint specification: reads clause . . . . . . . . . . . . . . .562.6.11 Specification Modules . . . . . . . . . . . . . . . . . . . . . . . . . . .57Pointers and physical addressing . . . . . . . . .
. . . . . . . . . . . . . . . .582.7.1Memory blocks and pointer dereferencing . . . . . . . . . . . . . . . .582.7.2Separation. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .592.7.3Dynamic allocation and deallocation . . . . . . . . . . . . . . . . . . .60Sets and lists . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . .642.8.1Finite sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .642.8.2Finite lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .65Abrupt termination. . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . .672.10 Dependencies information . . . . . . . . . . . . . . . . . . . . . . . . . . . . .692.11 Data invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .702.11.1 Semantics . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .712.11.2 Model variables and model fields . . . . . . . . . . . . . . . . . . . . .732.12 Ghost variables and statements . . . . . . . . . . . . . . . . . . . . .
. . . . .742.12.1 Volatile variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .782.13 Undefined values, dangling pointers . . . . . . . . . . . . . . . . . . . . . . . .792.13.1 Initialization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
.792.13.2 Dangling pointers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .792.14 Well-typed pointers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .806CONTENTS3 Libraries3.13.23.381Libraries of logic specifications . . . . . . . . . .
. . . . . . . . . . . . . . . .813.1.1Real numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .813.1.2Finite lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .813.1.3Sets and Maps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .81Jessie library: logical addressing of memory blocks . .
. . . . . . . . . . . . .823.2.1Abstract level of pointer validity . . . . . . . . . . . . . . . . . . . . .823.2.2Strings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .82Memory leaks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . .834 Conclusion85A Appendices87A.1 Glossary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .87A.2 Comparison with JML . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .87A.2.1 Low-level language vs. inheritance-based one . . . . . . . . . . . . . .88A.2.2 Deductive verification vs. RAC . . . . . .
. . . . . . . . . . . . . . . .91A.2.3 Syntactic differences . . . . . . . . . . . . . . . . . . . . . . . . . . . .92A.3 Typing rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .92A.3.1 Rules for terms . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . .92A.3.2 Typing rules for sets . . . . . . . . . . . . . . . . . . . . . . . . . . . .93A.4 Specification Templates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .93A.4.1 Accessing a C variable that is masked . . . . . . . . . . . . . . . .
. .93A.5 Illustrative example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .94A.6 Changes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101A.6.1 Version 1.12 . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 101A.6.2 Version 1.11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101A.6.3 Version 1.10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102A.6.4 Version 1.9 . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 102A.6.5 Version 1.8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102A.6.6 Version 1.7 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102A.6.7 Version 1.6 . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 102A.6.8 Version 1.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103A.6.9 Version 1.4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103A.6.10 Version 1.3 .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103A.6.11 Version 1.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103Bibliography1057CONTENTSList of Figures107Index1098CONTENTSForewordThis is the version 1.12 of ACSL design. Several features may still evolve in the future.
Inparticular, some features in this document are considered experimental, meaning that theirsyntax and semantics is not already fixed. These features are marked with Experimental.They must also be considered as advanced features, which are not supposed to be useful fora basic use of that specification language.AcknowledgementsWe gratefully thank all the people who contributed to this document: Sylvie Boldo, DavidCok, Jean-Louis Colaço, Pierre Crégut, David Delmas, Catherine Dubois, Stéphane Duprat,Arnaud Gotlieb, Philippe Herrmann, Thierry Hubert, André Maroneze, Dillon Pariente,Pierre Rousseau, Julien Signoles, Jean Souyris, Asma Tafat.9Chapter 1IntroductionThis document is a reference manual for ACSL.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
