问题涉及使用数学归纳法证明递归函数 presenza_strg 的正确性（评论为意大利语，对此表示抱歉）
/*Controlla in maniera ricorsiva se s1 è presente all'inizio di s2*/
/*Pre: s2 > s1 */
int presenza_strg(const char *s1, /*input - la stringa da ricercare*/
const char *s2) /*input - la stringa più grande*/
{
/*dichiarazione delle variabili locali alla funzione */
int risultato; /*output - risultato della verifica*/
if (*s1 == '\0')
risultato = 1; /*la stringa s1 è presente in s2*/
else if (*s1 != *s2)
risultato = 0; /*la stringa s1 NON è presente in s2*/
else
/*confronta i caratteri successivi delle due stringhe
(caso s1 == s2)*/
risultato = presenza_strg(s1 + 1,
s2 + 1);
return risultato;
}
该函数检查 s1 是否是 s2 的前缀，如果条件为 true，则返回 1，如果为 false，则返回 0
我已经尝试过如下证明，但它可能太令人困惑和费解：
待验证的财产：
如果我们将函数 presenza_strg(s1, s2) 的结果表示为 val(presenza)，并将 s1 和 s2 中包含的值分别表示为 val(s1) 和 val(s2)，那么：
val(s1) represents the value contained in s1, excluding the final \0 character.
val(s2) represents the value contained in s2 up to position n, where n is the length of s1.
我们想证明：
If val(presenza) = 1, then val(s1) == val(s2).
Alternatively, if val(presenza) = 0, then val(s1) != val(s2).
证明：
我们从基本情况 n = 0 开始，对 val(s1) 的长度 n 进行归纳。 如果 n = 0，则 s1 为空字符串，并且 val(s1) = ε （空字符串）。在这种情况下，满足条件 if (*s1 == ' ')，结果为 val(presenza) = 1。这里，val(s2) 也必须是 ε，因为我们从 s2 中提取长度为零的字符串.
现在假设条件在一定长度 n 内成立。我们想证明对于 n + 1 来说它仍然成立。
在第 n + 1 步，我们有三种可能的情况：
s1[n+1] (identifying the character at position n+1 of s1) is \0. The condition if (*s1 == '\0') is satisfied, so the result is val(presenza) = 1. Since s1 has reached the end (\0), the lengths of val(s1) and val(s2) remain equal to n. Given our assumption that up to length n, val(s1) == val(s2), this equality remains valid for n + 1.
s1[n+1] != s2[n+1]. The condition *s1 != *s2 is satisfied, and the result is val(presenza) = 0. In this case, val(s1) and val(s2) are different because the last character taken from s1 differs from the last character taken from s2. Thus, the condition val(s1) != val(s2) is correctly satisfied.
s1[n+1] == s2[n+1]. In this case, val(s1) = val(s2), and recursion continues to step n + 2.
总之，我们证明了假设条件 val(presenza) = 1 if val(s1) == val(s2) 或 val(presenza) = 0 if val(s1) != val(s2) 为真n，这个条件对于 n + 1 也成立。
教授写信给我说我验证的后置条件不正确（字面意思是“这不是要验证的后置条件”）。此时，我陷入困境，无法弄清楚为什么这是错误的或我实际上应该验证什么。 （老实说，我已经认为我能走到这一步已经是一个奇迹了。） 有人可以帮助我吗？预先感谢您。
在第 n + 1 步，我们有三种可能的情况：
…
s1[n+1] == s2[n+1]。在这种情况下，val(s1) = val(s2)，并且递归继续到步骤 n + 2。
这个没用；它证明不了什么。您已经证明，在这种情况下，在步骤 n+1，函数将继续执行步骤 n+2。所以呢？没有任何前提，也没有任何先前的证明表明该函数适用于步骤 n+2。
所以这个证明说“如果该函数适用于步骤n+2，那么它适用于步骤n+1”，但没有理由相信该函数适用于步骤n+2，所以有并不能证明该函数适用于所有步骤。
要进行归纳证明，您需要找到一些属性并证明该属性对于 n+1 成立，因为它对于 n （或更小）成立。