字符串的长度
函数 mystrlen(const char * const str) 计算 src 所指字符串的长度（字符数）。（验证时间约 3sec）
[Back to Index]
验证特点：字符串内置谓词，\is_pstring，循环变式
标注说明：函数前条件：函数入口处 str 所指向的是长度为 n 的物理字符串；
函数后条件：函数返回值等于 str 所指字符串的长度。
程序样例 
函数 mystrlen(const char * const str) 计算 src 所指字符串的长度（字符数）。（验证时间约 3sec）
验证特点：字符串内置谓词，\is_pstring，循环变式
标注说明：函数前条件：函数入口处 str 所指向的是长度为 n 的物理字符串；
函数后条件：函数返回值等于 str 所指字符串的长度。
程序样例