ACSL Mini Tutorial (811288), страница 3
Текст из файла (страница 3)
With this invariant, we can get rid of the terminates clause in the specification ofmax_list, since we are guaranteed that only finite lists will be passed to the function. Its specification will thusbe the following:/*@requires \valid(root);assigns \nothing;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);9.2Global InvariantsThere is another kind of data invariant in ACSL, called global invariant. As indicated by its name, a global invariantis a property of global variables that must hold at each entrance or exit of a function (for weak invariants) or ateach point of the program (for strong invariants).
For instance, suppose that we have a global list GList that is9.2 Global Invariantsalways non-empty and maintained in decreasing order, so that max_list(GList) can be replaced in the codeby if(GList) GList->element. A possible way to express that in ACSL is the following:/*@inductive sorted_decreasing{L}(list* root) {case sorted_nil{L}: sorted_decreasing(\null);case sorted_singleton{L}:\forall list* root;\valid(root) && root−>next == \null ==>sorted_decreasing(root);case sorted_next{L}:\forall list* root;\valid(root) && \valid(root−>next) &&root−>element >= root−>next−>element &&sorted_decreasing(root−>next) ==> sorted_decreasing(root);}*/list* GList;/*@ global invariant glist_sorted: sorted_decreasing(GList); */void insert_GList(int x);Because of the invariant of GList, a partial specification of insert_GList is that it can assume that GListis a sorted list, and that it must ensure that it is still the case when it returns.
A complete specification, for instancethat all the elements that were present at the entrance of the function are still there, and that x is present (insertedaccording to the ordering since the global invariant must still hold) can be expressed as such:/*@axiomatic Count {logic integer count(int x,list* l);axiom count_nil: \forall int x; count(x,\null) == 0;axiom count_cons_head{L}:\forall int x,list* l;\valid(l) && l−>element == x ==>count(x,l) == count(x,l−>next)+1;axiom count_cons_tail{L}:\forall int x, list* l;\valid(l) && l−>element != x ==>count(x,l) == count(x,l−>next);}*//*@ ensures \forall int y; y != x ==>count(y,GList) == count(y,\old(GList));ensures count(x,GList) == count(x,\old(GList))+1;*/void insert_GList(int x);13Chapter 10Verification activitiesThe preceding examples have shown us how to write the specification of a C function in ACSL.
However, atverification time, it can be necessary to write additional annotations in the implementation itself in order to guidethe analyzers.10.1AssertionsThe simplest form of code annotation is an assertion. An assertion is a property that must be verified each time theexecution reaches a given program point.
Some assertions may be discharged directly by one analyzer or another.When this happens, it means that the analyzer has concluded that there was no possibility of the assertion not beingrespected when the arguments satisfy the function’s pre-conditions. Conversely, when the analyzer is not able todetermine that an assertion always holds, it may be able to produce a pre-condition for the function that would, ifit was added to the function’s contract, ensure that the assertion was verified.In the following example, the first assertion can be verified automatically by many analyzers, whereas thesecond one can’t. An analyzer may suggest to add the pre-condition n > 0 to f’s contract./*@ requires n >= 0 && n < 100;*/int f(int n){int tmp = 100 − n;//@ assert tmp > 0;//@ assert tmp < 100;return tmp;}Let us now move on to a more interesting example.
The function sqsum below is meant to compute the sumof the squares of the elements of an array. As usual, we have to give some pre-conditions to ensure the validity ofthe pointer accesses, and a post-condition expressing what the intended result is:/*@ requires n >= 0;requires \valid(p+ (0..n−1));assigns \nothing;ensures \result == \sum(0,n−1,\lambda integer i; p[i]*p[i]);/*int sqsum(int* p, int n);A possible implementation is the following:int sqsum(int* p, int n) {int S=0, tmp;for(int i = 0; i < n; i++) {tmp = p[i] * p[i];S += tmp;10.2 Loop Invariants}return S;}This implementation seems to be correct with respect to the specification. However, this is not the case.
Indeed, the specification operates on mathematical (unbounded) integers, while the C statements uses moduloarithmetic within the int type. If there is an overflow, the post-condition will not hold. In order to overcomethis issue, a possible solution is to add some assertions before each int operation ensuring that there is no overflow. In the annotations, the arithmetic operations +,-,.
. . are the mathematical addition, substraction,. . . in theinteger domain. It is therefore possible to compare their results to INT_MAX. The code with its annotations isthe following:#include <limits.h>int sqsum(int* p, int n) {int S=0, tmp;for(int i = 0; i < n; i++) {//@ assert p[i] * p[i] <= INT_MAX;tmp = p[i] * p[i];//@ assert tmp >= 0;//@ assert S + tmp <= INT_MAX;S += tmp;}return S;}The assertion concerning tmp may be discharged automatically by some analyzers, but the other two assertions would require sqsum’s contract to be completed with additional pre-conditions.
Ideally, the necessarypre-conditions will be infered automatically from the assertions by an analyzer. Even if they are not, and if thepre-conditions need to be written by hand, it is still useful to write the assertions first. In cases like this one, itis easier to get the assertions right than the corresponding pre-conditions. Some analyzers may then be able tocheck that the assertions are verified under the pre-conditions, providing trust in the latter (In fact, to some analyzers, checking the assertions once the corresponding pre-conditions are provided is much easier than infering thepre-conditions from the assertions).10.2Loop InvariantsAnother kind of code annotations is dedicated to the analysis of loops. The treatment of loops is a difficult partof static analysis, and many analyzers need to be provided with hints in the form of an invariant for each loop.
Aloop invariant can be seen as a special case of assertion, which is preserved across the loop body. If we look backto the max_seq function, a useful invariant for proving that the implementation satisfies the formal specificationwould be that res contains the maximal value seen so far.Let us now try to formalize this invariant property.
Part of the formal invariant that we are trying to build isthat at any iteration j, the variable res is greater or equal to p[0],p[1],. . . ,p[j]. This part of the invariant iswritten:int max_seq(int* p, int n) {int res = *p;/*@ loop invariant \forall integer j;0 <= j < i ==> res >= *(\at(p,Pre)+j); */for(int i = 0; i < n; i++) {if (res < *p) { res = *p; }p++;}return res;}We use here the \at() construct, which is a generalization of \old.
Namely, it says that its argument mustbe evaluated in a given state of the program. A state is represented by a label, which can be a C label (the1510.2 Loop Invariantscorresponding state being the last time this label was reached) or some pre-defined logic labels. Pre indicatesthe pre-state of the function. \old is not admitted in loop invariant to avoid confusion with an evaluation at thebeginning of the previous loop step.The other part of the invariant property that should be expressed formally is that there exists an element inp[0],p[1],.
. . ,p[n-1] that is equal to res. In other words, this second part expresses that there exists aninteger e such that 0 <= e < n and p[e] == res. In order to prove the existence of such an integer e, thesimplest way is to keep track of the index for which the maximal value is attained. This can be done in ACSL withextra statements called ghost code. Ghost code is C code written inside //@ ghost .. or /*@ ghost .. */comments. The original program must have exactly the same behavior with and without ghost code. In other word,ghost code must not interfere with the concrete implementation.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
