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

final_progress ステートメントが証明されたにもかかわらず、Alt-Ergo/Z3 が「不明」または final_c アサーションのタイムアウトを生成するのはなぜですか? そのような明らかに（ユーザーの観点から）無効なステートメントについては、「無効」と表示したいと思います。

$ 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
4

1 に答える 1

1

WP プラグインは、プロパティ (事前条件、事後条件、ユーザー アサーション) を無効としてマークすることをサポートしていません。WP プラグイン マニュアルのセクション 2.2 に記載されているように、ステータスは次のいずれかです。

  1. 試したことのないアイコン— 証明は試みられていません。

  2. 不明なアイコン— プロパティは検証されていません。

    このステータスは、プルーフが見つからなかったことを意味します。これは、プロパティが実際には無効であることが原因である可能性があります。

  3. 仮説アイコンの下で有効— プロパティは有効ですが、依存関係があります。

    1 つ以上のプロパティが完全に有効であると仮定して、WP プラグインがプロパティを証明できる場合、このステータスがプロパティに適用されます。

  4. 確かに有効なアイコン— プロパティとそのすべての依存関係が完全に有効です。

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] 目標 typed_main_assert_false : 有効 (114ms) (97)
...

WP プラグインがassert \false有効とマークされている場合 (GUI では、有効だが依存関係があると表示されます)、無効なプロパティがあることがわかります。

于 2015-07-21T11:00:21.897 に答える