c - strstr 的 ACSL 契约(Contract)

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

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

/*@ 
    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 时成立。因此，您可能需要编写比您想要证明的那些更强大的不变量(因为那些可能不是归纳的)。