ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (1184405), страница 18
Текст из файла (страница 18)
The Function top stackThe function top stack is the runtime version of the logical function TopOfStack from Listing 8.5 on Page 116. The specification of top stack in Listing 8.27 simply states that for nonempty stacks top stack produces the same result as TopOfStack which in turn just returnsthe element obj[size-1] of Stack./*@requires IsValidStack(s);assigns \nothing;ensures IsValidStack(s);ensures !IsEmptyStack(s) ==> \result == TopOfStack(s);*/value_type top_stack(const Stack* s);Listing 8.27: Specification of top stackFor a non-empty stack the implementation of top stack in Figure 8.28 simply returns the element obj[size-1].
Note that our implementation of top stack does not crash when it isapplied to an empty stack. In this case we return the first element of the internal, non-empty arrayobj. This is consistent with our specification of top stack which only refers to non-emptystacks.value_type top_stack(const Stack* s){if (!empty_stack(s))return s->obj[s->size-1];elsereturn s->obj[0];}Listing 8.28: Implementation of top stack127Listing 8.29 shows our check whether top stack well-defined for non-empty stacks./*@requires IsValidStack(s) && !IsEmptyStack(s);requires IsValidStack(t) && !IsEmptyStack(t);requires IsEqualStack{Here,Here}(s, t);assigns \nothing;ensures \result;*/bool top_stack_ri(const Stack* s, const Stack* t){return top_stack(s) == top_stack(t);}Listing 8.29: Representation independence of top stackSince our axioms in Section 8.2 did not impose any restriction on the behavior of top_stack(s)for an empty s, it is sufficient to prove representation independence of top_stack(s) only fornonempty s.
This justifies the restricting ...&&!IsEmptyStack(...) in the first and secondrequires clause.1288.7.6. The Function push stackListing 8.30 shows the ACSL specification of the function push stack. In accordance withAxiom (8.5) push stack is supposed to increase the number of elements of a non-full stack byone. The specification also demands that the value that is pushed on a non-full stack becomesthe top element of the resulting stack (see Axiom (8.6)).
In addition to the requirements imposedby the axioms, our specification demands that push stack changes no memory location if it isapplied to a full stack./*@requires IsValidStack(s);assigns s->size;assigns s->obj[s->size];behavior not_full:assumes !IsFullStack(s);assigns s->size;assigns s->obj[s->size];ensuresensuresensuresensuresIsValidStack(s);SizeOfStack(s) == SizeOfStack{Old}(s) + 1;TopOfStack(s) == v;!IsEmptyStack(s);behavior full:assumes IsFullStack(s);assigns \nothing;ensures IsFullStack(s);complete behaviors;disjoint behaviors;*/void push_stack(Stack* s, value_type v);Listing 8.30: Specification of push stackThe implementation of push stack is shown in Listing 8.31.
It checks whether its argument isa non-full stack in which case it increases the field size by one but only after it has assigned thefunction argument to the element obj[size].void push_stack(Stack* s, value_type v){if (!full_stack(s))s->obj[s->size++] = v;}Listing 8.31: Implementation of push stack129Listing 8.32 shows our check whether push stack is well-defined. Since push stack doesnot return a value but rather modifies its argument we check whether it turns equal stacks intoequal stacks./*@requires IsValidStack(s);requires IsValidStack(t);requires IsEqualStack{Here,Here}(s, t);behavior not_full:assumes !IsFullStack(s);assignsassignsassignsassignsensuress->size;s->obj[s->size];t->size;t->obj[t->size];IsEqualStack{Here,Here}(s, t);behavior full:assumes IsFullStack(s);assigns \nothing;ensures IsEqualStack{Here,Here}(s, t);*/void push_stack_ri(Stack* s, Stack* t, value_type v){push_stack(s, v);push_stack(t, v);}Listing 8.32: Representation independence of push stack1308.7.7.
The Function pop stackListing 8.33 shows the ACSL specification of the function pop stack. In accordance withAxiom (8.7) pop stack is supposed to reduce the number of elements in a non-empty stackby one. In addition to the requirements imposed by the axioms, our specification demands thatpop stack changes no memory location if it is applied to an empty stack./*@requires IsValidStack(s);ensures IsValidStack(s);assigns s->size;behavior not_empty:assumes !IsEmptyStack(s);assigns s->size;ensures SizeOfStack(s) == SizeOfStack{Old}(s) - 1;ensures !IsFullStack(s);behavior empty:assumes IsEmptyStack(s);assigns \nothing;complete behaviors;disjoint behaviors;*/void pop_stack(Stack* s);Listing 8.33: Specification of pop stackThe implementation of pop stack is shown in Listing 8.34.
It checks whether its argument is anon-empty stack in which case it decreases the field size by one.void pop_stack(Stack* s){if (!empty_stack(s))--s->size;}Listing 8.34: Implementation of pop stack131Listing 8.35 shows our check whether pop stack is well-defined. Since pop stack does notreturn a value but rather modifies its argument we check whether it turns equal stacks into equalstacks./*@requires IsValidStack(s);requires IsValidStack(t);requires IsEqualStack{Here,Here}(s, t);assigns *s;assigns *t;ensures IsEqualStack{Here,Here}(s, t);*/void pop_stack_ri(Stack* s, Stack* t){pop_stack(s);pop_stack(t);}Listing 8.35: Representation independence of pop stack1328.8.
Verification of Stack AxiomsIn this section we show that the stack functions defined in Section 8.7 satisfy the stack axioms ofSection 8.2.8.8.1. Resetting a StackOur formulation in ACSL/C of the axiom in Equation (8.1) on Page 113 is shown in Listing 8.36.12345678910111213/*@requires IsValidStack(s);assigns *s;ensures IsValidStack(s);ensures \result == 0;*/size_type axiom_size_of_reset(Stack* s){reset_stack(s);return size_stack(s);}Listing 8.36: Specification of Axiom (8.1)1338.8.2. Adding an Element to a StackAxioms (8.5) and (8.6) describe the the behavior of a stack when an element is added.123456789101112131415/*@requires IsValidStack(s);requires !IsFullStack(s);assigns s->size;assigns s->obj[s->size];ensures IsValidStack(s);ensures \result == SizeOfStack{Old}(s) + 1;*/size_type axiom_size_of_push(Stack* s, value_type v){push_stack(s, v);return size_stack(s);}Listing 8.37: Specification of Axiom (8.5)Except for the assigns clauses, the ACSL-specification refers only to encapsulating logical functions and predicates defined in Section 8.4.
If ACSL would provide a means to define encapsulating logical functions returning also sets of memory locations, the expressions in assigns clauseswould not need to refer to the details of our Stack implementation.55 As an alternative, assignsclauses could be omitted, as long as the proofs are only used to convince a human reader.1234567891011121314/*@requires IsValidStack(s);requires !IsFullStack(s);assigns s->size;assigns s->obj[s->size];ensures \result == v;/*value_type axiom_top_of_push(Stack* s, value_type v){push_stack(s, v);return top_stack(s);}Listing 8.38: Specification of Axiom (8.6)55In [10, § 2.3.4], a powerful sublanguage to build memory location set expressions is defined, lacking, however, justfunction definitions.1348.8.3. Removing an Element from a StackAxioms 8.7, 8.8 and 8.9 describe the the behavior of a stack when an element is removed.12345678910111213141516/*@requiresrequiresrequiresrequiresIsEqualStack{Here,Here}(s, t);IsValidStack(s);IsValidStack(t);!IsFullStack(s);assigns s->size;assigns s->obj[s->size];ensures IsEqualStack{Here,Here}(s, t);*/void axiom_pop_of_push(Stack* s, Stack* t, value_type v){push_stack(s, v);pop_stack(s);}Listing 8.39: Specification of Axiom (8.8)The latter specification has been obtained in a fully systematical way.
In order to transform acondition equation p → s = t:• Generate a clause requires p.• Generate a clause requires x1 == ... == xn for each variable x with n occurrencesin s and t.• Change the i-th occurrence of x to xi in s and t.• Translate both terms s and t to reversed polish notation.• Generate a clause ensures y1 == y2, where y1 and y2 denote the value correspondingto the translated s and t, respectively.This makes it easy to implement a tool that does the translation automatically, but yields a slightlylonger contract in our example. For other data types, employing axioms with non-trivial left- andright-hand-sides (e.g.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
