KMP算法的next函数的证明
1.1 Next函数定义与代码
1.1.1 定义
1.1.2 实现代码
/*代码摘自《大话数据结构》*/
/*t为字串，next为int数组，存储next值*/
void getnext(string T,int *next)
{
int i,j;
i=1;j=0;next[1]=0;
while(i<T[0]) //T[0]表示字符串T的长度
{
if(j==0 || T[i]==T[j])
{
++i;
++j;
next[i]=j;
}
else
j=next[j];
}
}
1.2 证明思路
采取分段证明的办法，证明j往区间(m,k)移动是不正确的，验证移动到m（next[j]=m）的正确性。
在证明的过程中，都是假设j移动到某个位置之后，讨论if判断条件会成立。因为如果是不成立的话，程序流程又会转移到j的移动，这样我们就会陷入死循环。而且，这种假设，即if成立，在逻辑上也是成立的，就像递归函数一样，只要一层是正确的，递归的肯定也没问题。
1.3 证明
首先观察这个函数的代码，我们可以获得如下信息：
(1) 若if成立，则i、j都加1；
(2) i的值为k，则next[k]已经有了结果，且在下一轮if之前j= next[k]；
(3) 当要求next[k]的时候，if中的判断条件是i=k-1；
证明：
前提条件：假设next[k]=s,
即T[1]…[s-1]=T[k-s+1]…[k-1]（1）
现求next[k+1]=?根据前面的结论，此时i=k，j=s。令next[s]=m.
现进行if判断：
(1) 若条件成立，
即T[i]=T[j]，也即T[k]=T[s]，结合式（1），则有
T[1]…[s-1][s]=T[k-s+1]…[k-1][k] （2）
则next[k+1]=s+1，即代码中的next[i]=j;继续下一次if判断。
(2) 若条件不成立，
即T[i] != T[j]，则我们需要移动j。
假设向区间 (s , k) 移动，假使使j=s+1，满足if条件，即T[k]=T[s+1]，
根据代码，则next[k+1]=s+2，意味着
T[1]…[s-1][s][s+1]=T[k-s]…[k-1][k] （3）
等式两边去掉末位，
T[1]…[s-1][s] =T[k-s]…[k-1] （4）
从这可以推出next[k]=s+1，与前面矛盾，所以j不能向前移（假若向前移动更多位的话，就会推出next[k]比s+1更大的值）
下面证明j向（m，s）区间移动是不行的。
已知条件：i=k,j=s,next(s)=m,next(k)=s,T[k]!=T[s]，需证明移动到m+1是不行的。
现我们假设把j移动到m+1，而不是代码中的m。
根据已知条件可以得到：
next(k)=s =>T[1]…[s-1]=T[k-s+1]…[k-1] (5)
next(s)=m =>T[1]…[m-1]=T[s-m+1]…[s-1] (6)
if判断成立，T[k]=T[m+1]，则得到next(k+1)=m+2,
T[1]…[m+1]=T[k-m]…[k] (7)
两边去掉右边一位，则有T[1]…[m] =T[k-m]…[k-1] (8)
观察（5），因为s>=m+1,所以k-m>=k-s+1，
所以T[1]…[m] =T[k-m]…[k-1]
= T[s-m]…[s-1] （由5）
从这里可以推出，next(s)至少为m+1，与已知矛盾。
显然，若移动到m+2等就可以得到更大的next(s)的值了。
接下来，我们证明移动j到next[j]的正确性。
设next[j]=m，此时j=s，next[s]=m，移动j到next[s]后，即j=m。
由next[s]=m有：
T[1]…[m-1] =T[s-m+1]…[s-1] （9）
判断T[i]==T[j]，即T[k]==T[m]，条件成立之后，因为s>=m+1,所以
k-m+1>k-s+1，即T[k-m+1]在T[k-s+1]…[k-1][k]中。
取（1）中等式两边右边的m-1项，得到：
T[s-m+1]…[s-1] =T[(k-1)-(m-1)+1]…[k-1]= T[k-m+1]…[k-1] (10)
又结合（9）（10）有
T[1]…[m-1] =T[k-m+1]…[k-1] （11）
结合T[k]==T[m]，有
T[1]…[m-1][m]=T[k-m+1]…[k-1][k] (12)
从而next[k+1]=m+1，即代码中的next[i]=j。由next的定义可知，j向(0,m)区间移动的话就得不到正确的next值，应为已经找到了j=m满足要求，j值只能增大，减少就不符合定义。
至此，我们证明了把j回溯到大于m的任何位置都会得到错误的结论，且验证了移动到m可以得到正确的结论。