ACSL Mini Tutorial (811288), страница 2
Текст из файла (страница 2)
Moreover, the block pointed to by p must containat least n elements. In other words, p[0], p[1], ... p[n-1] must all be valid memory accesses. This is what thesecond requires clause expresses.The two ensures clauses display some similarities with the contract of the max function above: the result isgreater than or equal to every value in the sequence, and there exists an index for which the equality is attained.Note that the formulas in the post-condition only make sense under the assumption that the pre-condition holds:the validity condition ensures that it makes sense to speak about p[i], and if n could be 0, it would not be possibleto find an index where \result is attained.5.2Advanced specificationNote: This section can be skipped on a first readingIn addition, a more advanced ACSL construction allows to provide a shorter specification of max_seq: \maxis a built-in constructor (together with \min, \sum, and a few others), that returns the maximal value taken bya function in an interval of integers.
With \max and the \lambda construction to write functions as first-classexpressions, our specification becomes:/*@ requires n > 0 &&\valid(p + (0..n−1));ensures \result == \max(0,n−1,\lambda integer i; p[i]);/*int max_seq(int* p, int n);5.3ImplementationThe implementation of the max_seq function is pretty straightforward. For instance, we can use the followingcode.5.3 Implementationint max_seq(int* p, int n) {int res = *p;for(int i = 0; i < n; i++) {if (res < *p) { res = *p; }p++;}return res;}The specification we have given in the preceding section defines an expected behavior for the function max_seq.We will see later in this document that actually verifying that the function max_seq implements the specificationfrom the preceding section may require additional work.7Chapter 6Assigns clausesAs with the initial specification of max_ptr, an implementation of max_seq could zero all the locationsp[0],p[1],.
. . ,p[n-1], return zero, and would still satisfy the post-conditions in the specification from section 5.1. Again, we can use the \old keyword to avoid that./*@ requires n > 0;requires \valid(p+ (0..n−1));ensures \forall int i; 0 <= i <= n−1 ==> p[i] == \old(p[i]);ensures \forall int i; 0 <= i <= n−1 ==> \result >= p[i];ensures \exists int e; 0 <= e <= n−1 && \result == p[e];/*int max_seq(int* p, int n);It would be possible, but tedious, to use the same approach to specify that global variables do not change duringthe execution of max_seq. The ACSL language provides a special clause to specify that a function is not allowedto change memory locations other than the ones explicitly listed.
This clause is the assigns clause, and it is partof the function contract. When no assigns clauses are specified, the function is allowed to modify every visiblevariable. In presence of such clauses, the function can only modify the content of the locations that are explicitlymentioned in these clauses. In our case, we do not expect max_seq to have any visible side-effect, so that thecontract becomes:/*@ requires n > 0;requires \valid(p+ (0..n−1));assigns \nothing;ensures \forall int i; 0 <= i <= n−1 ==> \result >= p[i];ensures \exists int e; 0 <= e <= n−1 && \result == p[e];/*int max_seq(int* p, int n);Again, it is not necessary to use \old for the values of the expressions p[i] and p[e] in the the post-conditions,since the specification forces them to stay unchanged during the execution of max_seq.assigns clauses can be found in behaviors too.
Writing appropriate assigns clauses for p_minimum andq_minimum to complete the specification of max_ptr is left as an exercise for the reader.Chapter 7TerminationThere is yet another property that is implicitely expected from a satisfactory implementation of max_seq. Namely,this function, when called with arguments that satisfy its pre-conditions, should eventually terminate (and return aresult that satisfies its post-conditions).
The assigns clause in itself only guarantees that each time the functionterminates, only the specified locations may have been modified. Similarly, the post-conditions only apply whenthe function terminates, and so a function that never terminates would for instance satisfy the assigns andensures parts of the specification for max_seq. The termination of the function is a separate property that canbe specified in its contract using the terminates clause.Because in practice many functions are implicitely expected to terminate, the default in ACSL is to expectfunctions to terminate in all the contexts that satisfy their pre-conditions. It is possible to relax a particular function’s specification by providing a formula that describes the conditions in which the function is guaranteed toterminate.
An implementation is then allowed not to terminate when it is called in contexts that do not satisfy thiscondition.In the following example, the function f can be called with any argument c, but the function is not guaranteedto terminate if c<=0./*@assigns \nothing;terminates c>0;*/void f (int c) { while(!c); return;}Another valid contract for the same implementation of f is the following one, where the function implicitelyguarantees to terminate whenever it is called, but expects to be called only with non-zero arguments./*@requires c!=0;assigns \nothing;*/void f (int c) { while(!c); return;}Chapter 8Predicates and Logic FunctionsSo far, we have only used logical built-ins operators and relations.
It is often needed to define new logic predicatesand logic functions. For instance, if we define (simply) linked lists as such:typedef struct _list { int element; struct _list* next; } list;there are some common properties of lists that we want to be able to deal with in the logic. In particular,the notion of reachability (can a given node be attained from some root through a chain of next fields) plays animportant role. It can be defined in ACSL through the following annotation:/*@inductive reachable{L} (list* root, list* node) {case root_reachable{L}:\forall list* root; reachable(root,root);case next_reachable{L}:\forall list* root, *node;\valid(root) ==> reachable(root−>next, node) ==>reachable(root,node);}*/The notion of reachability is defined in ACSL by an inductive predicate.
Namely, root_reachable andnext_reachable can be seen as axioms indicating the cases under which reachable must hold, and the factthat reachable is inductive implies that these are the only cases under which it can hold. root_reachableindicates that reachable holds as soon as both its arguments are equal. next_reachable indicates that ifroot is valid and node can be proved reachable from root->next, then it is also reachable from root.The {L} notation indicates that the predicate takes as parameter a label, which represent a memory state ofthe program.
Indeed, as soon as we deal with pointers or arrays, we must refer to a particular memory state:reachable has no absolute meaning, it must be tied to a point of the program. In a case like this, there isno need to explicitely instantiate the label when we use reachable: the memory state to which it refers willusually be inferred from the context (e.g. for a precondition, it is the state at the start of the function, and for apost-condition, it is the state just before returning to the caller). More complex predicate may relate two or morememory states, but such definitions are out of scope in this tutorial.Now, the reachable predicate can be used to discriminate between circular and finite lists: in a finite list,we will ultimately reach \null;/*@ predicate finite{L}(list* root) = reachable(root,\null); */Here, it is not necessary to embed finite as inductive.
Instead, we directly give its definition in terms ofreachability.We can also note that finite is also parameterized by a label L. In fact, it is implicitely the memorystate in which reachable itself is evaluated. It would have been possible to make that explicit by writingreachable{L}(root,\null) instead, but this is not necessary here, as L denotes the only state in the environment at this level.11Similarly, we can define a logical function computing the length of a \null terminated list. This time, wehave to avoid circular lists, since the notion of length has little meaning for them. In order to do that, we can usean axiomatic:/*@ axiomatic Length {logic integer length{L}(list* l);axiom length_nil{L}: length(\null) == 0;axiom length_cons{L}:\forall list* l, integer n;finite(l) && \valid(l) ==>length(l) == length(l−>next) + 1;}*/An axiomatic is merely a set of logical declarations tied together. This way, it is possible to speak aboutlength(l) for any list l, but if l is circular, the value of this expression will remain undefined: the onlyway to prove that length(l)==n for a given n is to prove first finite(l).Now that we know how to define logic predicates and logic functions, we can go back to our maximumexample, this time on (finite) lists.
A possible specification for max_list would be the following:/*@requires \valid(root);assigns \nothing;terminates finite(root);ensures\forall list* l;\valid(l) && reachable(root,l) ==>\result >= l−>element;ensures\exists list* l;\valid(l) && reachable(root,l) && \result == l−>element;*/int max_list(list* root);As with arrays, we have as pre-condition that the list is non-empty. The post-conditions are also quite similar tothe ones of max_array, except that indices have been replaced by the reachability of the node from the root ofthe list. In addition, we find a terminates clause, that indicates that the implementation may loop forever oncircular lists (but could choose not to, even though this would imply an huge overhead in this setting).
A possibleimplementation is thus the following:int max_list(list* root) {int max = root−>element;while(root−>next) {root = root −> next;if (root−>element > max) max = root−>element;}return max;}Chapter 9Data InvariantsThis chapter can be skipped on a first reading.9.1Type InvariantsThe specification of the max_list function given above is complete, but it could be written differently. In fact, ifwe are writing a program that manipulates NULL-terminated linked lists, a lot a function will rely on the fact thatthe manipulated lists are finite. This means that each function must have a precondition or a terminates clausesimilar to the one of max_list, but also that the functions that build lists must ensure (with a post-condition)that the returned list is finite. Writing all these clauses might be tedious for a large set of functions.
Thus, ACSLprovide a way to express that all the elements of a given datatype respects some type invariants. By default, theseinvariants are weak invariants in the ACSL sense, that is, they must be valid at the entrance and at the exit of eachfunction, but can be temporarily broken inside a function’s body (provided they are restored before the functionreturns, or before calling another function which relies on them). ACSL has also a notion of strong invariant,which must hold at every point of the program, but they are harder to use in practice, and beyond the scope of thistutorial.In our list example, we can impose that each list is finite with the following annotation:/*@ type invariant finite_list(list* root) = finite(root); */The type invariant is a unary predicate. The type of its argument is the static type to which the invariant applies(in our case pointers to list).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
