ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (1184405), страница 2
Текст из файла (страница 2)
. . . . . . . . . . . . . . . .93958.5. The logical functions CapacityOfStack, SizeOfStack and TopOfStack8.6. Predicates for empty an full stacks . . . . . . . . . . . . . . . . . . . . . . . . .8.7. The predicate StackInvariants . . . . . . . . . . . . . . . . . . . . .
. . .8.8. The predicate IsValidStack . . . . . . . . . . . . . . . . . . . . . . . . . .8.9. Equality of stacks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8.11. Equality of stacks is an equivalence relation . . . . . . . . . . . . . . . . . . . .116117117117118119..........................................................................................................................................................9.....1. IntroductionFrama-C [3] is a suite of software tools dedicated to the analysis of C source code.Frama-C development efforts are conducted and coordinated at two French public institutions:CEA-LIST[4], a laboratory of applied research on software-intensive technologies and INRIASaclay[5], the French National Institute for Research in Computer Science and Control in collaboration with LRI[6], the Laboratory for Computer Science at Université Paris-Sud.Within Frama-C, the Jessie plug-in [2] enables deductive verification of C programs that havebeen annotated with the ANSI/ISO-C Specification Language (ACSL [1]).ACSL can express a wide range of functional properties.
The paramount notion inACSL is the function contract. While many software engineering experts advocatethe “function contract mindset” when designing complex software, they generallyleave the actual expression of the contract to run-time assertions, or to comments inthe source code. ACSL is expressly designed for writing the kind of properties thatmake up a function contract. [1]The Jessie plug-in uses Hoare-style weakest precondition computations to formally prove ACSLproperties of a program fragment.
Internally, Jessie relies on the languages and tools contained inthe Why platform [7]. Verification conditions are generated and submitted to external automatictheorem provers or interactive proof assistants.We at Fraunhofer FIRST [8] see the great potential for deductive verification using ACSL. However, we recognize that for a novice there are challenges to overcome in order to effectively use theJessie plug-in for deductive verification. In order to help users gain confidence, we have writtenthis tutorial that demonstrates how to write annotations for existing C programs. This documentprovides several examples featuring a variety of annotated functions using ACSL. For an in-depthunderstanding of ACSL, we strongly recommend users to read the official Frama-C introductorytutorial [9] first.
The principles presented in this paper are also documented in the ACSL referencedocument [10].1.1. AcknowledgmentMany members from the Frama-C community provided valuable input and comments during thecourse of the development of this document. In particular, we wish to thank our partners from theDevice-Soft5 project, Pascal Cuoq, Virgile Prevosto and Benjamin Monate, as well as the Jessiedevelopers, Claude Marché and Yannick Moy.5See http://www.first.fraunhofer.de/device_soft_en71.2. Structure of this DocumentThe functions presented in this document were selected from the C++ Standard Template Library(STL) [11]. The original C++ implementation was stripped from its generic implementation andmapped to C arrays of type value_type.Chapter 2 provides a short introduction into the Hoare Calculus.We have grouped the various STL algorithms in chapters as follows:• non-mutating algorithms (Chapter 3)• maximum/minimum algorithms (Chapter 4)• binary search algorithms (Chapter 5)• mutating algorithms (Chapter 6)• heap algorithms (Chapter 7)Using the example of a stack, we discuss in Chapter 8 how a datatype and its associated C functionscan be specified with ACSL.
Chapter 9 contains a summary of the results of the automatic theoremprovers employed for the deductive verification of the aforementioned examples.1.3. Types, Arrays, Ranges and Valid IndicesIn order to keep algorithms and specifications as general as possible, we use abstract type nameson almost all occasions. We currently defined the following types:typedef int value_type;typedef int size_type;typedef int bool;Programmers who know the types associated with STL containers will not be surprised thatvalue_type refers to the type of values in an array whereas size_type will be used for theindices of an array.This approach allows one to modify e.g. an algorithm working on an int array to work on a chararray by changing only one line of code, viz.
the typedef of value_type. Moreover, we believein better readability as it becomes clear whether a variable is used as an index or as a memory fora copy of an array element, just by looking at its type.The latter reason also applies to the use of bool. To denote values of that type, we #definedthe identifiers false and true to be 0 and 1, respectively. While any non-zero value is acceptedto denote true in ACSL like in C the algorithms shown in this tutorial will always produce 1for true. We omit clauses like \result == false || \result == true from our functioncontracts for sake of brevity only.
They still appear at places where they are needed for the provers,e.g. Listing 8.21. Due to the above definitions, the ACSL truth-value constant \false and \true8can be used interchangeably with our false and true, respectively, in ACSL clauses, but not inC code.Many of the algorithms, described in the following sections, rely on common principles. In thissection, we will list and explain their usage in finer detail.The C Standard describes an array as a “contiguously allocated nonempty set of objects” [12,§6.2.5.20]. If n is a constant integer expression with a value greater than zero, thenint a[n];describes an array of type int.
In particular, for each i that is greater than or equal to 0 and lessthan n, we can dereference the pointer a+i.Let the following prototype represent a function, whose first argument is the address to a rangeand whose second argument is the length of this range.void example(value_type* a, size_type n);To be very precise, we have to use the term range instead of array. This is due to the fact, thatfunctions may be called with empty ranges, i.e., with n == 0. Empty arrays, however, are notpermitted according to the definition stated above.
Nevertheless, we often use the term array andrange interchangeably.The following ACSL fragment expresses the precondition that the function example expects thatfor each i, such that 0 <= i < n, the pointer a+i may be safely dereferenced./*@requires 0 <= n;requires \valid_range(a, 0, n-1);*/void example(value_type* a, size_type n);In this case we refer to each index i with 0 <= i < n as a valid index of a.ACSL’s built-in predicate \valid_range(a, 0, n) refers to all addresses a+i where0 <= i <= n. However, the array notation int a[n] of the C programming language refersonly to the elements a+i where i satisfies 0 <= i < n.
Users of ACSL must therefore specify\valid_range(a, 0, n-1).In order to avoid this repeated writing of n-1 we introduce the predicate IsValidRange./*@predicate IsValidRange(value_type* a, integer n) =(0 <= n) && \valid_range(a, 0, n-1);*/Listing 1.1: The predicate IsValidRangeUsing IsValidRange allows us to shorten the specification of the function example to/*@requires IsValidRange(a, n);*/void example(value_type* a, size_type n);9The predicate IsValidRange will be frequently referenced in this document.1.4. Remarks on JessieJessie is a plug-in that takes ACSL specified C programs and performs deductive verification.Frama-C can be run using several Jessie options.Integer ModelsJessie knows different integer models:• exact, which means that C integers are considered to behave as unbounded integers in themathematical sense, i.e., ignoring the potential for an overflow.• bounded, which does not consider integers in the mathematical sense, but rather machinedependent integers.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
