基于KMP算法的字符串匹配搜索程序的验证（方案1）
该算法的实现主要包括两个方面：1) 计算用于搜索的目标字符串的部分匹配表table; 2) 在源字符串中匹配目标字符串。
算法描述请参见《数据结构（C语言版）》一书（严蔚敏、吴伟民著，清华大学出版社）。 （验证时间约 83sec）
[Back to Index]
验证特点：量化断言，幽灵代码，引理
标注说明：1. Create_KMP_Table函数：前条件：kmp表大小及目标物理字符串的长度；后条件：kmp表中的值满足字符串匹配的某种关系。
2. Search_Keyword函数：前条件：给定两个物理字符串；后条件：函数返回值等于串匹配的个数。
3. 使用量化断言描述字符串的匹配关系。
程序样例 
