ACSL - Can't prove function

Question

I'm trying to prove this function, but in vain. I'm also using another function, but I proved it.

Could anyone help me?

        I'm using Frama-C Sodium version with Alt-ergo 3 as prover.

  Given a not-empty string x.  An integer number p such that
    0 < p ≤|x| is meant to be "a period of x" if

      x[i] = x[i + p]

    for i = 0, 1, ... , |x| − p − 1.
    Note that, for each not-empty string, the length of the string
    is a period of itself.  In this way, every not-empty string
    has got at least one period.  So is well formed the concept of minimum
    period of string x, denoted by per(x):

      per(x) = min { p | p is period of x }.

    Write a C function

       unsigned per(const char x[], unsigned l)

    that, given a string x of length l, returns per(x). 

Here is the code and the specifications I have written so far:

/*@ 
    requires l > 0;
    requires p >= 0;

    behavior zero:
      assumes  p == l;
      ensures \result == 1;

    behavior one: 
      assumes l != p && (l%p) == 0;
      assumes \forall int i; 0 <= i < l-p-1 ==> x[i] == x[i+p];
      ensures \result == 1;

   behavior two:
      assumes l != p && (l%p) == 0;
      assumes !(\forall int i; 0 <= i < l-p-1 ==> x[i] == x[i+p]);
      ensures \result == 0;

   behavior three:
     assumes p != l && l%p != 0;
     ensures \result == 0;

   complete behaviors;
   disjoint behaviors;
*/

unsigned has_period(const char x[], unsigned int p, unsigned l) {
    if (p == l) return 1;
    if ((l % p) != 0) return 0;
        /*@
            loop assigns i;

            loop invariant \forall int j; 0 <= j < i ==> (x[j] == x[j+p]);
            loop invariant i <= l-p-1;
            loop invariant i >= 0;
        */

        for (int i = 0 ; i < l-p-1 ; ++i) {
            if (x[i] != x[i + p])
               return 0;
        }     

    return 1; 
}

/*
   predicate has_period(char* x, unsigned int p, unsigned l) =
      \forall int i; i < (l-p-1) ==>  x[i] == x[i+p]; 
*/

/*@
    requires l > 0;
    requires \valid(x+(0..l-1));

    ensures 1 <= \result <= l;
    ensures \forall unsigned int i; i < (l-\result-1) ==> x[i] == x[i+\result];
    ensures \forall unsigned int p; 1 <= p < \result ==> !(\forall int i; i < (l-p-1) ==> x[i] == x[i+p]);
*/

unsigned per(const char x[], unsigned l) {
     int p = 1;

    /*@
        loop assigns p;

        loop invariant 1 <= p <= l;
        loop invariant \forall unsigned j; 1 <= j < p ==> !(\forall int i; i < (l-j-1) ==> x[i] == x[i+j] || (l%p) == 0);
        loop invariant p >= 0;
    */

    while(p < l && !has_period(x,p,l)) 
        ++p;

    return p;
}

Answer 1

It would have helped if you had told us what your specific issue was, instead of a generic "it doesn't work", but here are some points:

• Your contracts are lacking assigns clause. These are not optional when using WP, especially for functions like has_period that are called within your development. WP needs those clauses to know which locations might have changed during the call, and by taking the complement, which locations have stayed the same.
• You have given a nice semi-formal definition of what a periodic string is. You should use that to define an ACSL predicate periodic (taking the same arguments as your C function has_period), and write your specifications according to this predicate. This will simplify your annotations a lot. In particular has_period does not need 4 behaviors: if periodic holds it must return 1, if periodic does not hold, it must return 0.
• Using -wp-rte leads to a bunch of unproved obligations. Depending on your assignment, you might want to strengthen your specifications, especially regarding the validity of the location pointed to by x.