c - Frama-C 字谜函数行为验证

Question

我编写了一个 C 函数，用于检查两个给定字符串(C 风格)是否是字谜词。我尝试用 Frama-C 验证它，但它无法验证函数的最终行为(其他规范有效)。 第一个超时(即使 WP 中的超时值非常高)，第二个未知。

这是代码:

    #include <string.h>
//@ ghost char alphabet[26] = {'a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i', 'j', 'k', 'l', 'm', 'n', 'o', 'p', 'q', 'r', 's', 't', 'u', 'v', 'w', 'x', 'y', 'z'};

/*@
    // Takes a character and return it to lowercase if it's uppercase
    axiomatic ToLower
    {
        logic char to_lower(char c);

        axiom lowercase:
            \forall char c; 97 <= c <= 122 ==> to_lower(c) == c;

        axiom uppercase:
            \forall char c; 65 <= c <= 90 ==> to_lower(c) == to_lower((char) (c+32));
    }
*/
/*@
    // Count the occurences of character 'c' into 'string' that is long 'n' characters
    axiomatic CountChar
    {
        logic integer count_char(char* string, integer n, char c);

        axiom count_zero:
            \forall char* string, integer n, char c; n <= 0 ==>
            count_char(string, n, c) == 0;

        axiom count_hit:
            \forall char* string, integer n, char c; n >= 0 && to_lower(string[n]) == c ==>
            count_char(string, n+1, c) == count_char(string, n, c) + 1;

        axiom count_miss:
            \forall char* string, integer n, char c; n >= 0 && to_lower(string[n]) != c ==>
            count_char(string, n+1, c) == count_char(string, n, c);
    }
*/

/*@
    predicate are_anagrams{L}(char* s1, char* s2) = ( \forall integer i; 0 <= i < 26 ==> 
    count_char(s1, strlen(s1), alphabet[i]) == count_char(s2, strlen(s2), alphabet[i]) );
*/

/*@
    requires valid_string(a);
    requires valid_string(b);

    // Requires that strings 'a' and 'b' are composed only by alphabet's letters and that are long equally.
    requires \forall integer k; 0 <= k < strlen(a) ==> 65 <= a[k] <= 90 || 97 <= a[k] <= 122;
    requires \forall integer k; 0 <= k < strlen(b) ==> 65 <= b[k] <= 90 || 97 <= b[k] <= 122;
    requires strlen(a) == strlen(b);

    ensures 0 <= \result <= 1;
    assigns \nothing;

    behavior anagrams:
    assumes are_anagrams(a, b);
    ensures \result == 1;
    behavior not_anagrams:
    assumes !are_anagrams(a, b);
    ensures \result == 0;
    complete behaviors anagrams, not_anagrams;
    disjoint behaviors anagrams, not_anagrams;
*/
int check_anagram(const char a[], const char b[])
{
   // Create two arrays and initialize them to zero
   int first[26];
   int second[26];
   int c;
   /*@
    loop assigns first[0..(c-1)];
    loop assigns second[0..(c-1)];
    loop assigns c; 
    loop invariant 0 <= c <= 26;
    loop invariant \forall integer k; 0 <= k < c ==> second[k] == first[k];
    loop invariant \forall integer k; 0 <= k < c ==> first[k] == 0 && second[k] == 0;
    loop invariant \valid(first+(0..25)) && \valid(second+(0..25));
    loop variant 26-c;
   */
   for(c = 0; c < 26; c++)
   {
      first[c] = 0;
      second[c] = 0;
   }

   char tmp = 'a';
   c = 0;

   // Now increment the array position related to position of character occured in the alphabet, subtracting ASCII decimal value of character from the character.
   /*@
    loop assigns first[0..25];
    loop assigns tmp;
    loop assigns c;
    loop invariant 97 <= tmp <= 122;
    loop invariant \valid(first+(0..25));
    loop invariant strlen(\at(a, Pre)) == strlen(\at(a, Here));
    loop invariant 0 <= c <= strlen(a);
    loop variant strlen(a)-c;
   */
   while (a[c] != '\0')
   {
      // This is a little trick to lowercase if the char is uppercase.
      tmp = (a[c] > 64 && a[c] < 91) ? a[c]+32 : a[c];
      first[tmp-97]++;
      c++;
   }


   c = 0;
   // Doing the same thing on second string.
   /*@
    loop assigns second[0..25];
    loop assigns tmp;
    loop assigns c;
    loop invariant 97 <= tmp <= 122;
    loop invariant \valid(second+(0..25));
    loop invariant strlen(\at(b, Pre)) == strlen(\at(b, Here));
    loop invariant 0 <= c <= strlen(b);
    loop variant strlen(b)-c;
   */
   while (b[c] != '\0')
   {
      tmp = (b[c] > 64 && b[c] < 91) ? b[c]+32 : b[c];
      second[tmp-'a']++;
      c++;
   }

   // And now compare the arrays containing the number of occurences to determine if strings are anagrams or not.
   /*@
    loop invariant strlen(\at(a, Pre)) == strlen(\at(a, Here));
    loop invariant strlen(\at(b, Pre)) == strlen(\at(b, Here));
    loop invariant 0 <= c <= 26;
    loop assigns c;
    loop variant 26-c;
   */
   for (c = 0; c < 26; c++)
   {
      if (first[c] != second[c])
         return 0;
   }

   return 1;
}

Answer 1

乍一看，您的规范似乎是正确的(但话又说回来，这是一个非常复杂的规范。我从未编写过任何如此复杂的 ACSL，因此我可能会遗漏一些东西)。

但是，函数 check_anagram 中的注释显然不足以解释为什么该函数应该遵守约定。特别要考虑 while 循环。为了真正了解函数的工作原理，每个循环的不变量应表示在任何迭代中，数组分别 first 和 second 包含计数到目前为止访问的第一个和第二个字符串的字符数。

这就是为什么在每个循环结束时，这些数组包含整个字符串的字符计数。

表达这些不变量将真正显示该函数是如何工作的。没有它们，就没有希望得出契约(Contract)执行的结论。