字符串的比较
函数 mystrcmp(const char* str1,const char* str2) 比较 str1 指向字符串和 str2 指向字符串的大小。（验证时间约 4sec）
程序中引入了使用逻辑函数的循环变式，证明程序的终止性。
[Back to Index]
验证特点：字符串内置谓词，\is_pstring
标注说明：函数前条件：描述待比较的两个字符串，并用逻辑变量记录它们；
函数后条件：（1）函数返回值等于0，则 str1 所指字符串和 str2 所指字符串相同；
（2）函数返回值大于0，则 str1 所指字符串大于 str2 所指字符串；
（3）函数返回值小于0，则 str1 所指字符串小于 str2 所指字符串。
程序样例 
