Inductive Proof for a Recursive Prefix Checking Function

Question

The problem involves proving, using mathematical induction, the correctness of the recursive function presenza_strg (comments are in italian sorry for that)

/*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;
}

The function checks whether s1 is a prefix of s2, returning 1 if the condition is true, or 0 if it is false

I have already attempted a proof as follows, but it might be too confusing and convoluted:

Property to Verify:

If we denote the result of the function presenza_strg(s1, s2) as val(presenza) and the values contained in s1 and s2 as val(s1) and val(s2) respectively, then:

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.

We want to prove that:

If val(presenza) = 1, then val(s1) == val(s2).
Alternatively, if val(presenza) = 0, then val(s1) != val(s2).

Proof:

We proceed by induction on the length n of val(s1), starting with the base case n = 0. If n = 0, then s1 is an empty string, and val(s1) = ε (the empty string). In this case, the condition if (*s1 == '\0') is satisfied, and the result is val(presenza) = 1. Here, val(s2) must also be ε since we are extracting a string of zero length from s2.

Now assume that the condition holds true up to a certain length n. We want to show that it remains true for n + 1.

At step n + 1, we have three possible cases:

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.

In conclusion, we have demonstrated that assuming the condition val(presenza) = 1 if val(s1) == val(s2) or val(presenza) = 0 if val(s1) != val(s2) is true up to n, this condition also holds true for n + 1.

The professor wrote to me saying that the postcondition I verified is incorrect (literally, "that's not the postcondition to verify"). At this point, I'm stuck and unable to figure out why it's wrong or what I should actually be verifying. (Honestly, I already consider it a miracle I got this far.). Could someone kindly help me? Thank you in advance.

Which is, according to you, the post condition? Did your professor say that your proof of that post condition is incorrect, or did your professor say that your choice of post condition is incorrect. The latter permits your proof is valid ( which it looks to be ), but that you have proved the wrong thing. — mevets
– mevets, Commented Jan 20 at 6:21

Eric Postpischil · Accepted Answer · 2025-01-20 12:11:13Z

At step n + 1, we have three possible cases:

…

s1[n+1] == s2[n+1]. In this case, val(s1) = val(s2), and recursion continues to step n + 2.

This is useless; it proves nothing. You have shown that, in this case, at step n+1, the function goes on to step n+2. So what? No premise and nothing proved earlier says the function works for step n+2.

So this proof says “If the function works for step n+2, then it works for step n+1,” but there is no reason to believe the function works for step n+2, so there is no proof the function works for all steps.

To make an inductive proof, you need to find some property and show the property holds for n+1 because it holds for n (or less). You need a property for which the n+1 case depends on the n case, not on the n+2 case.

You could do that by choosing a property that depends on string length. Prove the function works when the length of s1 is zero. Then prove that, if it works when the length of s1 is n, then it works if the length of s1 is n+1.

H.S. · Accepted Answer · 2025-01-20 17:23:51Z

Your inductive step should prove that if function presenza_strg() returns 1 for a string s1 of some arbitrary length n then it holds for length n + 1 as well, if string s1 is prefix of string s2.

Below in the post, ns1 is length of string s1 and ns2 is length of string s2.

Base Case:

ns1 = 0 i.e. s1 is an empty string. In this case, the condition *s1 == '\0' is satisfied, and presenza_strg() will return 1. Thus, behavior is correct for empty string.

If s1 is of length 1 and its a prefix of s2:

ns1 = 1 i.e. s1 is string of length 1. In this case, neither *s1 == '\0' nor *s1 != *s2 will satisfy. It make a recursive call - presenza_strg(s1 + 1, s2 + 1). Based on base case ns1 = 0, this recursive call will return 1.

Inductive Step:

Consider the case where the length of s1 is ns1 + 1 and ns2 >= ns1 + 1:

If neither *s1 == \0 nor *s1 != *s2 satisfy then the function presenza_strg() makes a recursive call to checks the next characters in the two strings. By the induction hypothesis, the recursive call presenza_strg(s1 + 1, s2 + 1) correctly checks if the s1 is a prefix of the rest of the string s2.

Hence, if presenza_strg(s1 + 1, s2 + 1) returns 1, then presenza_strg(s1, s2) will definitely return 1.

If *s1 == \0 satisfy but *s1 != *s2 doesn't then function presenza_strg() returns 0, indicates that s1 is not a prefix of s2.

Reference:

Mathematical Induction

Collectives™ on Stack Overflow

Inductive Proof for a Recursive Prefix Checking Function

2 Answers 2

Comments

Comments

Your Answer

Hot Network Questions

Collectives™ on Stack Overflow

2 Answers 2

Comments

Comments

Your Answer

Sign up or log in

Post as a guest

Related