-1

我有一个编程语言的函数，例如 C。我要求函数的输出满足某个条件。如果此函数的某些输入的输出不满足要求的条件，我需要找到任何这样的精确输入。

我通常需要这样做，但对于相当简单的功能，例如循环的数量是固定的并且不依赖于输入。另一个要求是我需要非常快地做到这一点。我发现 CBMC 工具 [https://www.cprover.org/cbmc/] 可能对我有帮助，但我不知道如何使用它。我也欢迎将问题转换为 CNF 公式的解决方案（但我仍然需要检索反例输入）。

函数示例：

int function(int n) {
    int m = 0;
    for(int i = 1; i < 8; i++) {
        m += n*i;
    }
    int output = m % 11;
    return output;
}
// POSTCONDITION: require the output < 10 for all inputs
// VERIFICATION: this is not true, the counterexample is the input n=9.
4

1 回答 1

0

考虑这个根本没有循环的简单函数：

bool function (int a, int b, int c)
{
   bool answer = a*a*a + b*b*b + c*c*c != 42;
   // POSTCONDITION: require answer==true
}

花了几百个计算机年（或者，在 500,000 个强大的 PC 网格上，实际上需要几周时间）才发现有一个反例（pdf）：

(-80538738812075974) 3 + 80435758145817515 3 + 12602123297335631 3 = 42

可以非常快地做到这一点的程序确实是一个非常非常好的程序。

于 2021-05-11T13:37:42.680 回答