ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (1184405), страница 17
Текст из файла (страница 17)
Equality of StacksDefining equality of instances of non-trivial data types, in particular in object-oriented languages,is not a trivial task. The book Programming in Scala[18, Chapter 28] devotes to this topic a wholechapter of more than twenty pages. In the following to sections we give a few hints how ACSLand Frama-C can help to correctly define equality for a simple datatype.We consider two stacks as equal if they have the same size and if they contain the same objects.Note that there is no need to compare the capacity of two stacks because in our setting all stackshave the same capacity (see Section 8.3). To be more precise, let s and t two pointers of typeStack, then we define the predicate IsEqualStack as in Listing 8.9./*@predicate IsEqualStack{S,T}(Stack* s, Stack* t) =SizeOfStack{S}(s) == SizeOfStack{T}(t) &&IsEqual{S,T}(\at(s->obj,S), SizeOfStack{S}(s), \at(t->obj,T));/*Listing 8.9: Equality of stacksNote that our use of labels in Listing 8.9 makes the specification fairly hard to read (in particularin the last line where we reuse the predicate IsEqual from Page 23).
However, this definitionof IsEqualStack will allow us later to compare the same stack object at different points ofa program. The logical expression IsEqualStack{S,T}(s,t) reads informally as “The stackobject s points to at program point S equals the stack object t points to at T”.A finer, but very important, point in our specification of equality of stacks is that the elements ofthe arrays s->obj and t->obj are compared only up to s->size and not up to s->capacity.Thus the two stacks s and t in Figure 8.10 are considered equal although there is an obviousdifference in their internal arrays.Stack s42capacity = 5size = 317 122Stack s4Figure 8.10.: Example of two equal stacks1182capacity = 5size = 31784If we define an equality relation (=) of objects for a data type such as Stack, we have to makesure that the following rules hold.reflexivitysymmetrytransitivity∀s ∈ S : s = s,(8.11a)∀s, t ∈ S : s = t =⇒ t = s,(8.11b)∀s, t, u ∈ S : s = t ∧ t = u =⇒ s = u.(8.11c)Any relation that satisfies the conditions (8.11) is referred to as an equivalence relation.
Themathematical set of all instances that are considered equal to some given instance s is called theequivalence class of s with respect to that relation.Listing 8.11 shows a formalization of these three rules for the relation IsEqualStack; it canbe automatically verified that they are a consequence of the definition of IsEqualStack inListing 8.9./*@lemma IsEqualStackReflexive{S} :\forall Stack* s; IsEqualStack{S,S}(s, s);lemma IsEqualStackSymmetric{S,T} :\forall Stack *s, *t;IsEqualStack{S,T}(s, t) ==> IsEqualStack{T,S}(t, s);lemma IsEqualStackTransitive{S,T,U}:\forall Stack *s, *t, *u;IsEqualStack{S,T}(s, t) && IsEqualStack{T,U}(t, u) ==>IsEqualStack{S,U}(s, u);*/Listing 8.11: Equality of stacks is an equivalence relationThe two stacks in Figure 8.10 show that the equivalence class of IsEqualStack can containmore than one element.51 The stacks s and t in Figure 8.10 are also referred to as two representatives of the same equivalence class.
In such a situation, the question arises whether a functionthat is defined on a set with an equivalence relation can be defined in such a way that its definitionis independent of the chosen representatives.52 We ask, in other words, whether the function arewell-defined on the set of all equivalence-classes wrt. IsEqualStack.53 The question of welldefinition will play an important role when verifying the functions of the Stack (see Section 8.7).51This is a common situation in mathematics. For example, the equivalence class of the rational number7infinite many elements, viz.
12 , 24 , 14, . . ..752This is why mathematicians have to prove that 21 + 53 equals 14+ 35 .53See http://en.wikipedia.org/wiki/Well-definition.12contains1198.6. Runtime Equality of StacksThe function equal stack is the C equivalent for the IsEqualStack predicate. The specification of equal stack is shown in Listing 8.12. Note that this specifications explicitly refersto valid stacks.123456789/*@requires IsValidStack(s);requires IsValidStack(t);assigns \nothing;ensures \result <==> IsEqualStack{Here,Here}(s, t);*/bool equal_stack(const Stack* s, const Stack* t);Listing 8.12: Specification of equal stackThe implementation of equal stack in Listing 8.13 compares two stacks according to the samerules as those of IsEqualStack.
The only difference is that we omit checking the constantStackCapacity.12345bool equal_stack(const Stack* s, const Stack* t){return (s->size == t->size) &&equal(s->obj, s->size, t->obj);}Listing 8.13: Implementation of equal stack1208.7. Verification of Stack FunctionsIn this section we verify the functions• reset stack, empty stack, full stack,• size stack, top stack, pop stack, and push stackof the data type Stack.
To be more precise, we provide for each of function foo stack:• an ACSL specification of foo stack• a C implementation of foo stack• a C function foo stack ri54 accompanied by a an ACSL contract that expresses thatthe implementation of foo stack is well-defined. Figure 8.14 shows our methodologyfor the verification of representation independence, (≈) again indicating the user-definedStack equality.Note, that the specifications of the various functions will explicitly refer to the internal state ofStack. In Section 8.8 we will show that the interplay of these functions fulfills the stack axiomsfrom Section 8.2.Specificationof pop/*@requires s ≈ t;requires !IsEmptyStack(s);...ensures s ≈ t;*/void pop_stack_ri(Stack *s, Stack *t){pop(s);pop(t);}Figure 8.14.: Methodology for verification of representation independence54The suffix ri stands for representation independence.1218.7.1.
The Function reset stackListing 8.15 shows the ACSL specification of reset stack. Note that our specification of thepost-conditions contains a redundancy because a stack is empty if and and only if its size is zero./*@requires IsValidStack(s);assigns s->size;ensures IsValidStack(s);ensures SizeOfStack(s) == 0;ensures IsEmptyStack(s);*/void reset_stack(Stack* s);Listing 8.15: Specification of reset stackListing 8.15 shows the implementation of reset stack. It simply sets the field size to zero.void reset_stack(Stack* s){s->size = 0;}Listing 8.16: Implementation of reset stackListing 8.15 shows the specification and implementation of our check that reset stack is welldefined.
Since reset stack changes the state of a stack, we check if the application of thisfunction turns equal stacks into equal stacks. Note that “Here” in the requires clause refers tothe state before calling reset stack ri() while the same identifier in the ensures clausesrefers to the state after calling./*@requires IsValidStack(s) && IsValidStack(t);requires IsEqualStack{Here,Here}(s, t);assigns s->size, t->size;ensures IsEqualStack{Here,Here}(s, t);*/void reset_stack_ri(Stack* s, Stack* t){reset_stack(s);reset_stack(t);}Listing 8.17: Representation independence of reset stack1228.7.2. The Function size stackThe function size stack is the runtime version of the logical function SizeOfStack fromListing 8.5 on Page 116.
The specification of size stack in Listing 8.18 simply states thatsize stack produces the same result as SizeOfStack which in turn just returns the fieldsize of Stack./*@requires IsValidStack(s);assigns \nothing;ensures IsValidStack(s);ensures \result == SizeOfStack(s);*/size_type size_stack(const Stack* s);Listing 8.18: Specification of size stackAs in the definition of the logical function SizeOfStack the implementation of size stackin Figure 8.19 simply returns the field size.size_type size_stack(const Stack* s){return s->size;}Listing 8.19: Implementation of size stackListing 8.20 shows our check whether size stack is well-defined. Since size stack neithermodifies the state of its Stack argument nor that of any global variable we only check whether itproduces the same result for equal stacks. Note that we simply may use “==” to compare integerssince we didn’t introduce a nontrivial equivalence relation on that data type./*@requires IsValidStack(s) && IsValidStack(t);requires IsEqualStack{Here,Here}(s, t);assigns \nothing;ensures \result;*/bool size_stack_ri(const Stack* s, const Stack* t){return size_stack(s) == size_stack(t);}Listing 8.20: Representation independence of size stack1238.7.3.
The Function empty stackThe function empty stack is the runtime version of the predicate IsEmptyStack from Listing 8.6 on Page 117./*@requires IsValidStack(s);assigns \nothing;ensures IsValidStack(s);ensures \result == true || \result == false;ensures \result <==> IsEmptyStack(s);*/bool empty_stack(const Stack* s);Listing 8.21: Specification of empty stackWe need to make sure that the result of empty_stack can only be true or false, that is 1 or0. If true could denote any nonzero value, we could not use the built-in == operator to check forrepresentation-independence in empty_stack_ri (Listing 8.23), since e.g. empty_stack(s)and empty_stack(t) could yield the value 2 and 4, respectively.
While both values denoteare evaluated as true in C, the comparison 2==4 fails. Defining a coarser equivalence relationas e.g. IsEqualBool(bool s, bool t) = (s != false <==> t != false), we couldavoid the above extra-ensures.As in the definition of the predicate IsEmptyStack the implementation of empty stack inFigure 8.22 simply checks whether the size of the stack is zero.bool empty_stack(const Stack* s){return size_stack(s) == 0;}Listing 8.22: Implementation of empty stack124Listing 8.23 shows our check whether empty stack is well-defined./*@requires IsValidStack(s);requires IsValidStack(t);requires IsEqualStack{Here,Here}(s, t);assigns \nothing;ensures \result;*/bool empty_stack_ri(const Stack* s, const Stack* t){return empty_stack(s) == empty_stack(t);}Listing 8.23: Representation independence of empty stack1258.7.4. The Function full stackThe function full stack is the runtime version of the predicate IsFullStack from Listing 8.6 on Page 117./*@requires IsValidStack(s);assigns \nothing;ensures IsValidStack(s);ensures \result == true || \result == false;ensures (\result) <==> IsFullStack(s);*/bool full_stack(const Stack* s);Listing 8.24: Specification of full stackAs in the definition of the predicate IsFullStack the implementation of full stack in Figure 8.25 simply checks whether the size of the stack equals its capacity.bool full_stack(const Stack* s){return size_stack(s) == StackCapacity;}Listing 8.25: Implementation of full stackListing 8.26 shows our check whether full stack is well-defined./*@requires IsValidStack(s);requires IsValidStack(t);requires IsEqualStack{Here,Here}(s, t);assigns \nothing;ensures \result;*/bool full_stack_ri(const Stack* s, const Stack* t){return full_stack(s) == full_stack(t);}Listing 8.26: Representation independence of full stack1268.7.5.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
