在不知道f的实现的情况下，你只能对全部的输入进行测试。
for (i = INT_MIN; i <= INT_MAX; i++) {if (f(i)) {printf ("f return none zero value");break;}}
另外也可以借助SMT求解器验证，不过要把函数转换成SMT求解器能理解的格式。
例如对于这个函数：
int func(int x) {if (x * x - 129 == 0) {return 1;} else {return x - x;}}
转化成：
func :: SInt64 -> SInt64func x = ite (x * x - 129 .== 0) -- if1 -- then子句(x - x) -- else子句
SMT求解器很快就能找到一个反例，证明func的返回值不是始终为0：
ghci> import Data.SBV.Bridge.Z3ghci> prove $ forAll ["x"] $ x -> func x .== 0Falsifiable. Counter-example:x = 4219259137745094591 :: SInt64
（因为对于64位的int，4219259137745094591 * 4219259137745094591 = 129）
如果是黑盒的话，考虑对输入进行穷举或者随机测试
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
暂无简介
文章 0 评论 0
接受
发布评论
评论（2）
在不知道f的实现的情况下，你只能对全部的输入进行测试。
for (i = INT_MIN; i <= INT_MAX; i++) {
if (f(i)) {
printf ("f return none zero value");
break;
}
}
另外也可以借助SMT求解器验证，不过要把函数转换成SMT求解器能理解的格式。
例如对于这个函数：
int func(int x) {
if (x * x - 129 == 0) {
return 1;
} else {
return x - x;
}
}
转化成：
func :: SInt64 -> SInt64
func x = ite (x * x - 129 .== 0) -- if
1 -- then子句
(x - x) -- else子句
SMT求解器很快就能找到一个反例，证明func的返回值不是始终为0：
ghci> import Data.SBV.Bridge.Z3
ghci> prove $ forAll ["x"] $ x -> func x .== 0
Falsifiable. Counter-example:
x = 4219259137745094591 :: SInt64
（因为对于64位的int，4219259137745094591 * 4219259137745094591 = 129）
如果是黑盒的话，考虑对输入进行穷举或者随机测试