ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver (1185160)
Текст из файла
ACSL Version 1.9Implementation in Sodium-20150201ACSL: ANSI/ISO C SpecificationLanguageVersion 1.9 – Sodium-20150201Patrick 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-91405©2009-2013 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 . . . . . . . . . . . . . . . . . . . . . . . . . .121.2.1Kinds of annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . .121.2.2Parsing annotations in practice . .
. . . . . . . . . . . . . . . . . . . .131.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 . . . . . . . . . . . . . . . . . .262.2.8String literals . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . .28Function contracts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .282.3.1Built-in constructs \old and \result . . . . . . . . . . . . . . . . . . . .292.3.2Simple function contracts . . . .
. . . . . . . . . . . . . . . . . . . . .302.3.3Contracts with named behaviors . . . . . . . . . . . . . . . . . . . . .312.3.4Memory locations and sets of terms . . . . . . . . . . . . . . . . . . .342.3.5Default contracts, multiple contracts . . .
. . . . . . . . . . . . . . . .35Statement annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .362.4.1Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .362.4.2Loop annotations . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . .362.32.45CONTENTS2.4.3Built-in construct \at . . . . . . . . . . . . . . . . . . . . . . . . . . .412.4.4Statement contracts . . . . . . . . . . . . . . . . . . . . . . . . . . . .43Termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .442.5.1Integer measures .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .452.5.2General measures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .452.5.3Recursive function calls . . . . . . . . . . . . . . . . . . . . . . . . . .462.5.4Non-terminating functions . . . . . . . . . . . . . . . . . . . . . .
. . .47Logic specifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .472.6.1Predicate and function definitions . . . . . . . . . . . . . . . . . . . .482.6.2Lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .492.6.3Inductive predicates . . .
. . . . . . . . . . . . . . . . . . . . . . . . .492.6.4Axiomatic definitions. . . . . . . . . . . . . . . . . . . . . . . . . . .502.6.5Polymorphic logic types . . . . . . . . . . . . . . . . . . . . . . . . . .512.6.6Recursive logic definitions . . . . . . . . . . . . . . . . . . . . . . . . .512.6.7Higher-order logic constructions .
. . . . . . . . . . . . . . . . . . . . .522.6.8Concrete logic types . . . . . . . . . . . . . . . . . . . . . . . . . . . .532.6.9Hybrid functions and predicates . . . . . . . . . . . . . . . . . . . . .542.6.10 Memory footprint specification: reads clause . . . . . . . . . . . . . . .552.6.11 Specification Modules . . . . . . . . . . . .
. . . . . . . . . . . . . . .56Pointers and physical adressing . . . . . . . . . . . . . . . . . . . . . . . . . .572.7.1Memory blocks and pointer dereferencing . . . . . . . . . . . . . . . .572.7.2Separation. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .592.7.3Dynamic allocation and deallocation . . . . . . . . . . . . . . . . . . .592.8Sets as first-class values . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . .632.9Abrupt termination. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .642.10 Dependencies information . . . . . . . . . . . . . . . . . . . . . . . . . . . . .662.11 Data invariants . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .672.11.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .682.11.2 Model variables and model fields . . . . . . . . . . . . . . . . . . . . .702.12 Ghost variables and statements . . . . . . . . . . . . . . . . . . . .
. . . . . .722.12.1 Volatile variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .752.13 Undefined values, dangling pointers . . . . . . . . . . . . . . . . . . . . . . . .762.13.1 Initialization . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . .762.13.2 Dangling pointers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .772.52.62.76CONTENTS3 Libraries3.13.23.379Libraries of logic specifications . . . . . . . . . . . . . . . . . . . . . . . . . .793.1.1Real numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
.793.1.2Finite lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .793.1.3Sets and Maps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .79Jessie library: logical addressing of memory blocks . . . . . . . . . . . . . . .803.2.1Abstract level of pointer validity . . . . . . . . . .
. . . . . . . . . . .803.2.2Strings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .80Memory leaks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .814 Conclusion83A Appendices85A.1 Glossary . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . .85A.2 Comparison with JML . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .85A.2.1 Low-level language vs. inheritance-based one . . . . . . . . . . . . . .86A.2.2 Deductive verification vs. RAC . . . . . . . . . . . . . . . . . . . . . .89A.2.3 Syntactic differences .
. . . . . . . . . . . . . . . . . . . . . . . . . . .90A.3 Typing rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .90A.3.1 Rules for terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .90A.3.2 Typing rules for sets . . . . . . . .
. . . . . . . . . . . . . . . . . . . .91A.4 Specification Templates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .91A.4.1 Accessing a C variable that is masked . . . . . . . . . . . . . . . . . .91A.5 Illustrative example . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . .92A.6 Changes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .99A.6.1 Version 1.9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .99A.6.2 Version 1.8 . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . .99A.6.3 Version 1.7 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100A.6.4 Version 1.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100A.6.5 Version 1.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100A.6.6 Version 1.4 .
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
