尽管有确凿的论断，但SMT证明者的产量仍然“未知" [英] SMT prover yields 'unknown' despite strong proven assertions

问题描述

假设我们有以下带有C注释的代码:

Suppose we have the following C annotated code:

#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;
}

为什么尽管final_progress语句得到了证明，但Alt-Ergo/Z3对于final_c断言仍会产生未知"或超时? 对于从用户的角度来看这样明显的无效语句，我肯定希望看到无效".

Why Alt-Ergo/Z3 yields "unknown" or timeouts for final_c assertion despite the fact that final_progress statement was proven? I would definitely like to see "Not valid" for such obviously (from user point of view) invalid statements.

$ 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

推荐答案

WP插件不支持将标记属性(前提条件，后置条件，用户断言)标记为无效.如 WP插件手册的第2.2节所述，状态是以下之一:

The WP plugin does not support marking properties (preconditions, postconditions, user assertions) as invalid. As documented in section 2.2 of the WP plugin manual, the status is one of:

1. —没有尝试证明.

2. —该属性尚未通过验证.

1. — No proof attempted.

2. — The property has not been validated.

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

This status means that a proof could not be found. This might be because the property is actually invalid.

>-该属性有效，但具有依赖性.

— The property is valid but has dependencies.

如果WP插件能够假设一个或多个属性完全有效，那么您将看到此状态应用于该属性.

You will see this status applied to a property if the WP plugin is able to prove the property assuming one or more properties are fully valid.

—该属性及其所有依赖项都是完全有效的.

— The property and all its dependencies are fully valid.

尽管WP插件不支持将属性标记为无效，但是您可以使用在函数末尾声明\false的技巧:

Although the WP plugin does not support marking properties as invalid, you can use the trick of asserting \false at the end of the function:

#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插件会导致:

Running the WP plugin on this code results in:

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

如果WP插件将assert \false标记为有效(在GUI中将显示为"valid-but-has-dependencies")，那么您知道存在无效的属性.

If the WP plugin marks assert \false valid (in the GUI it will show as valid-but-has-dependencies) then you know that there is an invalid property.

这篇关于尽管有确凿的论断，但SMT证明者的产量仍然“未知"的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！