查找破坏输出后置条件的函数的输入

如何解决查找破坏输出后置条件的函数的输入

我有一个编程语言的函数，例如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.

解决方法

考虑这个完全没有循环的简单函数：

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 网格上实际花费了几周时间）才发现存在一个 counterexample (pdf)：

(−80538738812075974)³ + 80435758145817515³ + 12602123297335631³ = 42

能够非常快地完成这项工作的程序确实是一个非常非常好的程序。