字符串的ACSL合同

Question

我正在尝试为一个C函数编写一个规范，该函数可以搜索一个字符串在另一个字符串中的第一个匹配项(实际上是string .h的strstr函数)。

我遇到的第一个问题是我不能证明循环不变量，我认为我使用strlen (在__fc_string_axiomatic.h中定义的公理)的方式有问题。

#include<string.h>
/*@ 
    requires valid_string(s1);
    requires valid_string(s2);

*/
char *strfind (const char *s1, const char *s2) {
  if (*s2 == 0) 
      return s1;
  /*@ 
    loop invariant 0 <= s1 - \at(s1,Pre) <= strlen(\at(s1,Pre));
  */
  while (*s1) { 
    const char *rs1 = s1;
    const char *rs2 = s2;
    /*@ 
        loop invariant 0 <= rs1 - s1 <= strlen(s1);
        loop invariant 0 <= rs2 - s2 <= strlen(s2);
    */
    while (*rs1 && *rs2 && (*rs1 == *rs2)) { 
        rs1++; 
        rs2++; 
    }
    if (*rs2 == 0) 
        return s1;
    s1++;
  }
  return 0;
}

Answer 1

你的循环不变量是正确的(我成功地证明了它们)，但它们太弱了，你应该加强它们。这是我用Frama-C的WP插件证明的函数的一个版本，Frama C是杰西的继承者。

/*@ 
    requires valid_string(s1);
    requires valid_string(s2);
*/
char *strfind (const char *s1, const char *s2) {
  if (*s2 == 0) 
      return s1;
  /*@ 
    loop invariant valid_string(s1);
    loop invariant strlen(\at(s1,Pre)) == (s1 - \at(s1,Pre)) + strlen(s1);
    loop invariant 0 <= s1 - \at(s1,Pre) <= strlen(\at(s1,Pre));
    loop assigns s1;
  */
  while (*s1) { 
    const char *rs1 = s1;
    const char *rs2 = s2;
    /*@ 
        loop invariant valid_string(rs1);
        loop invariant valid_string(rs2);
        loop invariant strlen(\at(s1,Pre)) == (rs1 - \at(s1,Pre)) + strlen(rs1);
        loop invariant strlen(s2) == (rs2 - s2) + strlen(rs2);
        loop invariant 0 <= rs1 - s1 <= strlen(s1);
        loop invariant 0 <= rs2 - s2 <= strlen(s2);
        loop assigns rs1, rs2;
    */
    while (*rs1 && *rs2 && (*rs1 == *rs2)) { 
        rs1++; 
        rs2++; 
    }
    if (*rs2 == 0) 
        return s1;
    s1++;
  }
  return 0;
}

首先，注意在valid_string上添加的循环不变量。如果没有它们，证明者就不能确定strlen(s1/rs1/rs2)是否仍然是正的，因为指针可能在字符串结束后增加了。

接下来，我添加了与\at(s1,Pre)、s1和它们各自的长度相关的等式。这些比你的不等式的正确部分更强，并被用来证明上述不等式--使用假设valid_string(s1)，它确保了strlen(s1)>=0。

不等式的左边部分是适当的循环不变量，并且可以在最初证明(没有任何额外的不变量)。

记住，对于所有的K，前K个循环不变量必须是归纳的。这意味着，在它们在迭代i中成立的假设下，您应该能够证明它们在迭代i+1中成立。因此，您可能需要编写比您想要证明的不变量更强的不变量(因为它们可能不是归纳的)。