ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (1184405), страница 16
Текст из файла (страница 16)
The Stack Data TypeOriginally, ACSL is tailored to the task of specifying and verifying one single C function at a time.However, in practice we are also faced with the task to implement a family of functions, usuallyaround some sophisticated data structure, which have to obey certain rules of interdependence.In this kind of task, we are not interested in the properties of a single function (usually called“implementation details”), but in properties describing how several function play together (usuallycalled “abstract interface description”, or “abstract data type properties”).This chapter introduces a methodology to formally denote and verify the latter property sets usingACSL.
The only data type so far discussed is Stack.A stack is a data type that can hold objects and has the property that, if an object a is pushed ona stack before object b, then a can only be removed (popped) after b. A stack is, in other words,a first-in, last-out data type (see Figure 8.1). The top function of a stack returns the last elementthat has been pushed on a stack.pushpoptopbaFigure 8.1.: Push and pop on a stackWe consider only stacks that have a finite capacity, that is, that can only hold a maximum number cof elements that is constant throughout their lifetime.
This restriction allows us to define a stackwithout relying on dynamic memory allocation. When a stack is created or reset, it contains noelements, i.e., its size is 0. The function push and pop increases and decreases the size of a stackby at most one, respectively.1118.1. Methodology OverviewFigure 8.2 gives an overview of our methodology to specify and verify abstract data types (verification of one axiom shown only).⌝full(s) ➞ pop(push(s, v)) = sAxiom 8.8/*@Implementationof popImplementationof pushSpecificationof popSpecificationof pushrequires s ≈ t;requires !IsFullStack(s);...ensures s ≈ t;*/voidaxiom_8_8(Stack* s, Stack* t, value_type v){push(s, v);pop(s);}Figure 8.2.: Methodology OverviewWhat we will basically do is:1. specify axioms about how the stack functions should interact with each other (Section 8.2),2. define a basic implementation of C data structures (only one in our example, viz.struct Stack; see Section 8.3) and some invariants the instances of them have to obey(Section 8.4),3.
provide for each stack function an ACSL contract and a C implementation (Section 8.7),4. verify each function against its contract (Section 8.7),5. transform the axioms into ACSL-annotated C code (Section 8.8), and6. verify that code, using access function contracts and data-type invariants as necessary (Section 8.8).Section 8.5 provides an ACSL-predicate deciding whether two instances of a struct Stackare considered to be equal (indication by “≈” in Figure 8.2), while Section 8.6 gives a corresponding C implementation.
The issue of an appropriate definition of equality of data instances isfamiliar to any C programmer who had to replace a faulty comparison if(s1==s2) by the correctif(strcmp(s1,s2)==0) to compare two strings char *s1,*s2 for equality.1128.2. Stack AxiomsTo specify the interplay of the stack access functions, we use a set of axioms, each of which hasthe form of a conditional equation.49Let V denote an arbitrary type. We denote by S c the type of stacks with capacity c > 0 of elementsof type V. The aforementioned functions then have the following signatures.reset : S c → S c ,push : S c × V → S c ,pop : S c → S c ,top : S c → V,size : S c → N.With B denoting the boolean type we will also define two auxiliary functionsempty : S c → B,full : S c → B.To qualify as a stack these functions must satisfy the following rules which are also referred to asstack axioms.8.2.1.
Resetting a StackAfter a stack has been reset its size is 0.size(reset(s)) = 0.(8.1)The auxiliary functions empty and full are defined as followsempty(s),iffsize(s) = 0,(8.2)full(s),iffsize(s) = c.(8.3)We expect that for every stack s the following condition holds0 ≤ size(s) ≤ c.49(8.4)There is an analogy in geometry: Euclid (e.g. [16]) invented the use of axioms there, but still kept definitions ofpoint, line, plane, etc. Hilbert [17] recognized that the latter are not only unformalizable, but also unnecessary, anddropped them, keeping only the formal descriptions of relations between them.1138.2.2. Adding an Element to a StackTo push an element v on a stack the stack must not be full.
If an element has been pushed on aneligible stack, its size increases by 1size(push(s, v)) = size(s) + 1,if¬full(s).(8.5)Moreover, the element pushed on a stack is the top element of the resulting stacktop(push(s, v)) = v,if¬full(s).(8.6)8.2.3. Removing an Element from a StackAn element can only be removed from a non-empty stack. If an element has been removed froman eligible stack the stack size decreases by 1size(pop(s)) = size(s) − 1,if¬empty(s).(8.7)If an element is pushed on a stack and immediately afterwards an element is removed from theresulting stack then the final stack is equal to the original stackpop(push(s, v)) = s,if¬full(s).(8.8)Conversely, if an element is removed from a non-empty stack and if afterwards the top element ofthe original stack is pushed on the new stack then the resulting stack is equal to the original stack.push(pop(s), top(s)) = s,if¬empty(s).(8.9)8.2.4.
A Note on Exception HandlingWe don’t impose a requirement on push(s,v) if s is a full stack, nor on pop(s) or top(s) if sis an empty stack. Specifying the behavior in such exceptional situations is a problem by its own;a variety of approaches is discussed in the literature. We won’t elaborate further on this issue, butonly give an example to warn about “innocent-looking” exception specifications that may lead toundesired results.If we’d introduce an additional error value err in the element type V and require top(s) = errif s is empty, we’d be faced with the problem of specifying the behavior of push(s,err). Atfirst glance, it would seem a good idea to have err just been ignored by push, i.e.
to requirepush(s, err) = s.(8.10)However, we then could derive for any non-full and non-empty stack s, that===size(s)size(pop(push(s,err)))size(pop(s))size(s) - 1by 8.8as assumed in 8.10by 8.7i.e. no such stacks could exist, or all int values would be equal.1148.3. The struct Stack and its Associated FunctionsWe now introduce one possible C implementation of the above axioms. It is centered around theC structure Stack shown in Listing 8.3.#define StackCapacity 8struct Stack{value_type obj[StackCapacity];size_type};size;typedef struct Stack Stack;Listing 8.3: Definition of struct StackThis struct holds an array obj of non-zero length called StackCapacity. Please note that allour Stack objects have the same constant capacity.
The field size indicates the number elementsthat are currently in the stack. See also Figure 8.4 which attempts to interpret this definitionaccording to Figure 8.1....obj[size-1]...top ofstackStackCapacitysizeobj[1]obj[0]Figure 8.4.: Interpretation of Stack115Based on the stack functions from Section 8.2, we declare the following access functions as partof our Stack data type.voidreset_stack(Stack* s);boolequal_stack(const Stack* s, const Stack* t);size_typesize_stack(const Stack* s);boolempty_stack(const Stack* s);boolfull_stack(const Stack* s);value_typetop_stack(const Stack* s);voidpush_stack(Stack* s, value_type v);voidpop_stack(Stack* s);Most of these functions directly correspond to methods of the C++ std::stack template class.50The function equal stack corresponds to the comparison operator ==, whereas one use ofreset stack is to bring a stack into a well-defined initial state.
The function full stack hasno counterpart in std::stack. This reflects the fact that we avoid dynamic memory allocation,while std::stack does not.8.4. Stack InvariantsNot every possible instance of struct Stack is considered a valid one, e.g., with our definitionof StackCapacity in Listing 8.3, Stack s={{0},999} is not. Below, we will define an ACSLpredicate StackInvariants discriminating valid and invalid instances.Before, we introduce in Listing 8.5 the two auxiliary logical functions CapacityOfStack andSizeOfStack with which we can refer in specifications to the constant StackCapacity andthe field size of Stack, respectively.
This listing also contains the logical function TopOfStackwhich defines the array element with index size-1 as the top element of a stack. The reader canconsider this as an attempt to hide implementation details from the specification./*@logic size_type CapacityOfStack{L}(Stack* s) =(size_type)StackCapacity;logic size_type SizeOfStack{L}(Stack* s) = s->size;logic value_type TopOfStack{L}(Stack* s) = s->obj[s->size-1];*/Listing 8.5: The logical functions CapacityOfStack, SizeOfStack and TopOfStack50See http://www.sgi.com/tech/stl/stack.html116We also introduce in Listing 8.6 two predicates that express the concepts of empty and full stacksby referring to a stack’s size and capacity (see Equations (8.2) and (8.3))./*@predicate IsEmptyStack{L}(Stack* s) = SizeOfStack(s) == 0;predicate IsFullStack{L}(Stack* s) =SizeOfStack(s) == CapacityOfStack(s);*/Listing 8.6: Predicates for empty an full stacksThere are some obvious invariants that must be fulfilled by every valid object of type Stack:• The stack capacity shall be strictly greater than zero (an empty stack is ok but a stack thatcannot hold anything is not useful).• The pointer obj shall refer to an array of length capacity.• The number of elements size of a stack the must be non-negative and not greater than itscapacity.These invariants are formalized in the predicate StackInvariants of Listing 8.7.
Note howthe use of the previously defined logical functions and predicates (including the predicateIsValidRange from Listing 1.1 on Page 9) allows us to define the stack invariant without directlyreferring to the fields of Stack./*@predicate StackInvariants{L}(Stack* s) =0 < CapacityOfStack(s) &&0 <= SizeOfStack(s) <= CapacityOfStack(s) &&IsValidRange(s->obj, CapacityOfStack(s));*/Listing 8.7: The predicate StackInvariantsAs we usually have to deal with a pointer s of type Stack we add a predicate that combines thenecessary valid(s) with the stack invariant (see Listing 8.8)./*@predicate IsValidStack{L}(Stack* s) =\valid(s) && StackInvariants(s);*/Listing 8.8: The predicate IsValidStack1178.5.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
