首页 文章

尽管有很强的证据，SMT证明者仍然会产生'unknown'

提问于
浏览 次
2

假设我们有以下C注释代码：

#define L  3
int a[L] = {0};
/*@ requires \valid(a+(0..(L - 1)));
    ensures \forall int j; 0 <= j < L ==> (a[j] == j); */
int main() {
        int i = 0;
        /*@ loop assigns i, a[0..(i-1)];
            loop invariant inv1: 0 <= i <= L;
            loop invariant inv2:
                        \forall int k; 0 <= k < i ==> a[k] == k; 
        */
        while (i < L) {
          a[i] = i;
          i++;
        }
        /*@ assert final_progress:
               \forall int k; 0 < k < L ==> a[k] == a[k-1] + 1; 
            assert final_c: 
               a[2] == a[1] - 1; */
        return 0;
}

为什么Alt-Ergo / Z3为final_c断言产生“未知”或超时，尽管final_progress语句已被证实？对于这样明显（从用户的角度来看）无效语句，我肯定希望看到“无效” .

$ frama-c -wp -wp-rte -wp-prover z3 test2.c
..
[wp] [z3] Goal typed_main_assert_final_c : Unknown (455ms)

$ frama-c -wp -wp-rte -wp-prover alt-ergo test2.c 
..
[wp] [Alt-Ergo] Goal typed_main_assert_final_c : Timeout
z3 verification frama-c alt-ergo

1 回答

  • 1

    WP插件不支持将属性（前置条件，后置条件，用户断言）标记为无效 . 如WP plugin manual第2.2节所述，状态为以下之一：

    never tried icon

    • 未尝试任何证据 .

    unknown icon

    • 该 properties 尚未经过验证 .

    此状态表示无法找到证据 . 这可能是因为该属性实际上是无效的 .

    valid under hypothesis icon

    • 该属性有效但具有依赖项 .

    如果WP插件能够在假设一个或多个属性完全有效的情况下证明该属性，则会看到此状态应用于属性 .

    surely valid icon

    • 属性及其所有依赖项完全有效 .

    虽然WP插件不支持将属性标记为无效，但您可以在函数末尾使用断言 \false 的技巧：

    #define L  3
int a[L] = {0};
/*@ requires \valid(a+(0..(L - 1)));
    ensures \forall int j; 0 <= j < L ==> (a[j] == j); */
int main()
{
    int i = 0;
    /*@ loop assigns i, a[0..(i-1)];
        loop invariant inv1: 0 <= i <= L;
        loop invariant inv2: \forall int k; 0 <= k < i ==> a[k] == k; 
    */
    while (i < L) {
        a[i] = i;
        i++;
    }
    //@ assert final_progress: \forall int k; 0 < k < L ==> a[k] == a[k-1] + 1;
    //@ assert final_c: a[2] == a[1] - 1;
    //@ assert false: \false;
    return 0;
}

    在此代码上运行WP插件会导致：

    ...
[wp] [Alt-Ergo] Goal typed_main_assert_false : Valid (114ms) (97)
...

    如果WP插件标记 assert \false 有效（在GUI中它将显示为有效但具有依赖性），那么您知道存在无效属性 .

    回复于

相关问题