数组中大于0的元素个数
给定整型数组t，求数组中大于0的元素个数。（验证时间约4sec）
[Back to Index]
验证特点：高阶逻辑构造：范域词 \numof，for 循环，循环变式，引理
引理的引入是为了协助定理证明器实现数值计算是否上溢出的证明。
标注说明：函数前条件：说明整形数组的长度；
函数后条件：利用范域词给出程序的返回值为数组中元素大于0的个数。
程序样例 
给定整型数组t，求数组中大于0的元素个数。（验证时间约4sec）
验证特点：高阶逻辑构造：范域词 \numof，for 循环，循环变式，引理
引理的引入是为了协助定理证明器实现数值计算是否上溢出的证明。
标注说明：函数前条件：说明整形数组的长度；
函数后条件：利用范域词给出程序的返回值为数组中元素大于0的个数。
程序样例