ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов.pdf)
Описание файла
PDF-файл из архива "ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов.pdf", который расположен в категории "". Всё это находится в предмете "практика" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
ACSL By ExampleTowards a Verified C Standard LibraryVersion 5.1.1for Frama-C BoronFebruary 2011Jochen BurghardtJens GerlachLiangliang GuKerstin HartigHans PohlJuan SotoKim VöllingerThis body of work was completed within the Device-Soft project1 , which is supported by theProgramme Inter Carnot Fraunhofer from BMBF (Grant 01SF0804) and ANR.Except where otherwise noted, this work is licensed underhttp://creativecommons.org/licenses/by-nc-sa/3.0/12See http://www.first.fraunhofer.de/device_soft_enForewordThis report provides various examples for the formal specification, implementation, and deductiveverification of C programs using the ANSI/ISO-C Specification Language (ACSL [1]) and theJessie plug-in [2] of Frama-C [3] (Framework for Modular Analysis of C programs).We have chosen our examples from the C++ Standard Library whose initial version is still knownas the Standard Template Library (STL).2 The STL contains a broad collection of generic algorithms that work not only on C arrays but also on more elaborate containers, i.e., data structures.For the purposes of this document we have selected representative algorithms, and converted theirimplementation from C++ function templates to C functions that work on arrays of type int.3In March 2009, while working in the context of the ES PASS4 ITEA2 project, we released aninitial version of this report.
This earlier edition referred to the Lithium release of Frama-C. Thereport at hand is a completely revised and extended edition that refers to the Boron release of theFrama-C.We plan to extend this report in later releases by describing additional STL algorithms. Thus, stepby step, this document will evolve from an ACSL tutorial to a report on a formally specified anddeductively verified Standard Library for ANSI/ISO-C.
Moreover, should ACSL be extended toa C++ specification language, our work may be extended to a deductively verified C++ StandardLibrary.You may email comments, suggestions or errors todevicesoft@first.fraunhofer.deIn particular, we encourage you to check vigilantly whether our formal specifications capture theessence of the informal description of the STL algorithms.We appreciate your feedback and hope that this document helps foster the adoption of deductiveverification techniques.2See http://www.sgi.com/tech/stl/We are not directly using int in the source code but rather value_type which is a typedef for int.4See http://www.es-pass.org33Contents1.
Introduction1.1.1.2.1.3.1.4.7Acknowledgment . . . . . . . . . . . .Structure of this Document . . . . . . .Types, Arrays, Ranges and Valid IndicesRemarks on Jessie . . . . . . . . . . . .........................................................................................2. The Hoare Calculus2.1.2.2.2.3.2.4.2.5.2.6.The Assignment RuleThe Sequence Rule .The Implication RuleThe Choice Rule . .The Loop Rule . . .Derived Rules .
. . .13................................................................................................................................................................................................The equal Algorithm . . . . . . .The mismatch Algorithm . . . . .The find Algorithm . . . . . .
. .The find Algorithm ReconsideredThe find first of Algorithm .The adjacent find Algorithm .The count Algorithm . . . . . . .The search Algorithm . . . . . .................................................................................................................................................................................................element Algorithm .
. . . . . . . .element Algorithm with Predicatesseq Algorithm . . . . . . . . . . . .element Algorithm . . . . . . . . .........................................................................3. Non-mutating Algorithms3.1.3.2.3.3.3.4.3.5.3.6.3.7.3.8.The maxThe maxThe maxThe min2226283032343638415.
Binary Search Algorithms5.1. The lower bound Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . .5.2. The upper bound Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . .5.3. The binary search Algorithm . . . . . . . . . . . . . . . . . . . . . . . . .6. Mutating Algorithms6.1. The fill Algorithm .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6.2. The swap Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6.3. The swap values Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . .4141616161719214. Maximum and Minimum Algorithms4.1.4.2.4.3.4.4.788104345474951525456596062646.4.6.5.6.6.6.7.6.8.6.9.6.10.6.11.The swap ranges Algorithm .
. . . . . . . . .The copy Algorithm . . . . . . . . . . . . . . .The reverse copy and reverse algorithms .The rotate copy Algorithm . . . . . . . . . .The replace copy Algorithm . . . . . . . . .The remove copy Algorithm . . . . . . . .
. .The unique copy Algorithm . . . . . . . . . .The iota Algorithm . . . . . . . . . . . . . . ................................................................................................................................................................................................................................................................7. Heap Operations7.1.7.2.7.3.7.4.7.5.7.6.7.7.Axiomatic Description of Heaps . .The is heap Algorithm . .
. . . .The push heap Algorithm . . . .The pop heap Algorithm . . . . .The make heap Algorithm . . . .The sort heap Algorithm . . . .The Sorting Algorithm heap sort91.................................................8. The Stack Data Type8.1.8.2.8.3.8.4.8.5.8.6.8.7.8.8.Methodology Overview . .
. . . . . . . . . . . . .Stack Axioms . . . . . . . . . . . . . . . . . . . .The struct Stack and its Associated FunctionsStack Invariants . . . . . . . . . . . . . . . . . . .Equality of Stacks . . . . . . . . . . . . . . . . . .Runtime Equality of Stacks . . . .
. . . . . . . . .Verification of Stack Functions . . . . . . . . . . .Verification of Stack Axioms . . . . . . . . . . . .................................................................................................................................New in Version 5.1.1 (February 2011) . .
. . . . . . . . . . . .New in Version 5.1.0 (May 2010) . . . . . . . . . . . . . . . . .New in Version 4.2.2 (May 2010) . . . . . . . . . . . . . . . . .New in Version 4.2.1 (April 2010) . . . . . . . . . . . . . . . .New in Version 4.2.0 (January 2010) . . . . . . . . . . . . . . .Unofficial Release as part of the ES PASS project (March 2009)112113115116118120121133137A. ChangesBibliography9394981011061081101119. Results from Deductive VerificationA.1.A.2.A.3.A.4.A.5.A.6.6670727678808488143......................................................1431431431441441441455List of Predicates, Logic Functions andLemmata1.1.
The predicate IsValidRange . . . . . . . . . . . . . . . . . . . . . . . . . . .3.2. The predicate IsEqual . . . . . . . .3.11. The predicate HasValue . . . . . . .3.14. The predicate HasValueOf . . . . . .3.17. The predicate HasEqualNeighbors3.20. Axiomatic definition of Count . . . . .3.23. The predicate HasSubRange . . . . .6................................................2330323436384.1. Operator < defines a partial order on value_type . . . . . . . .
. . . . . . . .4.2. Semantics of derived comparison operators . . . . . . . . . . . . . . . . . . . .4.5. The IsMaximum and IsFirstMaximum predicates . . . . . . . . . . . . . .4142455.1. The predicate IsSorted . . . . . . . . . . . . . . . . . . . . . . . . .
. . . .5.2. Axiomatic Description of Division . . . . . . . . . . . . . . . . . . . . . . .51516.5. The predicate SwapValues . . . . . . . . . . . . .6.22. Axiomatic of the logic function WhitherRemove6.23. The predicate RemoveCopy . . . . . . . . . . .
.6.26. The Logic Function WhitherUnique . . . . . . .6.28. The Predicate UniqueCopy . . . . . . . . . . . ......64818284867.2. The ParentChild and IsHeap predicates . . . . . . . . . . . . . . . . . . . .7.4. The predicates Even and Odd. . . . . . . . . . . .
