ACSL - не может доказать функцию

Question

Я пытаюсь доказать эту функцию, но тщетно. Я тоже использую другую функцию, но я это доказал.

Кто-нибудь может мне помочь?

        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). 

Вот код и спецификации, которые я написал до сих пор:

/*@ 
    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

Это помогло бы, если бы вы сказали нам, в чем заключается ваша конкретная проблема, вместо общего "это не работает", но вот некоторые моменты:

• Ваши контракты отсутствуют assigns пункт. Они не являются обязательными при использовании WP, особенно для таких функций, как has_period которые называются в вашем развитии. WP нужны эти пункты, чтобы знать, какие местоположения могли измениться во время разговора, и, взяв дополнение, какие местоположения остались прежними.
• Вы дали хорошее полуформальное определение того, что такое периодическая строка. Вы должны использовать это для определения предиката ACSL periodic (принимая те же аргументы, что и ваша функция C has_period), и напишите свои спецификации в соответствии с этим предикатом. Это значительно упростит ваши аннотации. Особенно has_period не нужно 4 поведения: если periodic держит это должно вернуться 1, если periodic не держит, он должен вернуть 0,
• С помощью -wp-rte приводит к куче недоказанных обязательств. В зависимости от вашего назначения, вы можете усилить свои спецификации, особенно в отношении обоснованности местоположения, на которое указывает x,