递归前缀检查函数presenza_strg归纳证明：后置条件验证错误求助

函数定义 #

该C函数用于检查s1是否是s2的前缀，是则返回1，否则返回0，前置条件为s2长度大于等于s1：

/*递归检查s1是否是s2的前缀*/
/*前置条件：s2长度大于s1*/
int presenza_strg(const char *s1, /*输入 - 待查找的字符串*/
                  const char *s2) /*输入 - 更长的字符串*/
{
    /*声明函数局部变量 */
    int risultato; /*输出 - 验证结果*/

    if (*s1 == '\0')
        risultato = 1; /*s1是s2的前缀*/
    else if (*s1 != *s2)
        risultato = 0; /*s1不是s2的前缀*/
    else
        /*比较两个字符串的下一个字符（s1当前字符等于s2当前字符的情况）*/
        risultato = presenza_strg(s1 + 1, 
                                  s2 + 1); 

    return risultato;
}

原证明的问题 #

你提出的待验证性质存在两个核心错误：

1. val(s2)的定义不符合递归逻辑：你将val(s2)固定为s2前n个字符（n为原s1的长度），但递归过程中每次调用的s1和s2都是指针偏移后的子串，此时需要验证的是当前子串的前缀关系，而非原字符串的固定长度匹配。
2. 性质表述未准确对应函数功能：函数的本质是验证「s1的全部字符（直到\0）与s2的前m个字符完全匹配（m为s1的长度）」，原性质的表述没有明确递归子问题的前缀关系，导致归纳步骤逻辑混乱。

正确的后置条件与归纳证明 #

正确的待验证性质 #

对于任意字符串指针s1、s2（满足前置条件：原s2长度≥原s1长度），调用presenza_strg(s1, s2)返回1 当且仅当 从当前s1指针开始的子串是从当前s2指针开始的子串的前缀。

数学归纳法证明 #

归纳变量

设m为当前s1指针到其末尾\0的字符数（即当前子串的长度，不含\0），对m进行归纳。

基例（m=0）

此时s1指向\0，函数直接返回1。空串是任何字符串的前缀，符合性质，基例成立。

归纳假设

假设当m=k（k≥0）时，性质成立：即调用presenza_strg(s1, s2)返回1当且仅当s1开始的k长度子串是s2开始的k长度子串的前缀。

归纳步骤（m=k+1）

此时s1指向的不是\0，分两种情况讨论：

• 情况1：当前字符不匹配（*s1 != *s2）
  函数返回0。由于s1的第一个字符与s2的第一个字符不同，显然s1的k+1长度子串不可能是s2的前缀，符合性质。
• 情况2：当前字符匹配（*s1 == *s2）
  函数递归调用presenza_strg(s1+1, s2+1)。此时s1+1开始的子串长度为k，s2+1开始的子串长度≥k（满足前置条件）。根据归纳假设：
  • 若递归返回1：说明s1+1的k长度子串是s2+1的k长度子串的前缀，结合当前字符匹配，可知s1的k+1长度子串是s2的前缀，函数返回1，符合性质。
  • 若递归返回0：说明s1+1的k长度子串不是s2+1的k长度子串的前缀，因此s1的k+1长度子串也不是s2的前缀，函数返回0，符合性质。

两种情况均满足性质，归纳步骤成立。

综上，函数presenza_strg的正确性得证。

内容的提问来源于stack exchange，提问作者Nicola Pirozzi