字符串的连接
函数 mystrcat(char* dest, const char* src) 连接两个字符串，将 src 指向的字符串拼接到 dest 指向的字符串的末尾，覆盖 dest 指向字符串尾的 '\0'。（验证时间约 17sec）
[Back to Index]
验证特点：字符串内置谓词，\is_pstring，\length，\offset
标注说明：函数前条件：src 和 dest 分别指向长度为 n 和 m 的字符串。字符数组dest的长度大于 m+n。
逻辑变量 oldsrc 和 olddest 分别记录函数入口处 src 和 dest 的值；
函数后条件：函数出口处字符数组 dest 的内容是长度分别为 m、n 的两个逻辑字符串 olddest 和 oldsrc 的拼接。src 的字符串没有改变。
程序样例 
