ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver
Описание файла
PDF-файл из архива "ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver", который расположен в категории "". Всё это находится в предмете "формальная спецификация и верификация программ" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
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 .
