2

2つのループ不変条件を証明するのに問題があります：

    loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m2)[i] == \at(((char*)m1)[i], Pre);
    loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m1)[i] == \at(((char*)m2)[i], Pre);

\atが期待どおりに配列に対して機能していないと思います。

ACSL by Example（68ページ、swap_ranges）にも同様の関数があり、これを使用していますが、前述のように、WPプラグインでこの特定の関数を証明することはできませんでした。私は自分のマシンでそれを試しましたが、実際に同じ不変条件を証明することはできません。

完全なコード

/*
 * memswap()
 *
 * Swaps the contents of two nonoverlapping memory areas.
 * This really could be done faster...
 */

#include "string.h"

/*@
    requires n >= 1;
    requires \valid(((char*)m1)+(0..n-1));
    requires \valid(((char*)m2)+(0..n-1));
    requires \separated(((char*)m1)+(0..n-1), ((char*)m2)+(0..n-1));
    assigns ((char*)m1)[0..n-1];
    assigns ((char*)m2)[0..n-1];
    ensures \forall integer i; 0 <= i < n ==> ((char*)m1)[i] == \old(((char*)m2)[i]);
    ensures \forall integer i; 0 <= i < n ==> ((char*)m2)[i] == \old(((char*)m1)[i]);
@*/
void memswap(void *m1, void *m2, size_t n)
{
    char *p = m1;
    char *q = m2;
    char tmp;

    /*@
        loop invariant 0 <= n <= \at(n, Pre);
        loop invariant p == m1+(\at(n, Pre) - n);
        loop invariant q == m2+(\at(n, Pre) - n);
        loop invariant (char*)m1 <= p <= (char*)m1+\at(n, Pre);
        loop invariant (char*)m2 <= q <= (char*)m2+\at(n, Pre);
        loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m2)[i] == \at(((char*)m1)[i], Pre);
        loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m1)[i] == \at(((char*)m2)[i], Pre);
        loop assigns n, tmp, ((char*)m1)[0..\at(n,Pre)-1], ((char*)um2)[0..\at(n, Pre)-1], p, q;
        loop variant n;
    @*/
    while (/*n--*/ n) {
        tmp = *p;
        *p = *q;
        *q = tmp;

        p++;
        q++;

        n--; // inserted code
    }
}

編集

Frama-C Oxygenリリースを使用しており、alt-ergo（0.94）およびcvc3（2.4.1）を使用して自動証明を試しました

frama-cからの出力：

cvc3：

[wp] [Cvc3] Goal store_memswap_loop_inv_7_established : Valid
[wp] [Cvc3] Goal store_memswap_loop_inv_6_established : Valid
[wp] [Cvc3] Goal store_memswap_loop_inv_7_preserved : Unknown
[wp] [Cvc3] Goal store_memswap_loop_inv_6_preserved : Unknown

alt-ergo：

[wp] [Alt-Ergo] Goal store_memswap_loop_inv_7_established : Valid
[wp] [Alt-Ergo] Goal store_memswap_loop_inv_6_established : Valid
[wp] [Alt-Ergo] Goal store_memswap_loop_inv_7_preserved : Timeout
[wp] [Alt-Ergo] Goal store_memswap_loop_inv_6_preserved : Timeout
4

1 に答える 1

5 
/*@
…
    loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m2)[i] == \at(((char*)m1)[i], Pre);
    loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m1)[i] == \at(((char*)m2)[i], Pre);
    loop assigns n, tmp, ((char*)m1)[0..\at(n,Pre)-1], ((char*)um2)[0..\at(n, Pre)-1], p, q;
…
@*/

あなたは間違っていloop assignsます。loop assigns注釈は、各反復で変更されたメモリ位置を示します。通常、場所の数はループが進むにつれて増加します（この場合はn減少します）。それは次のようなものです：

loop assigns n, tmp, ((char*)m1)[0..(\at(n, Pre) - n - 1)], ((char*)um2)[0..(\at(n, Pre) - n - 1)], p, q;

しかし、上記の私自身の提案は、一方向または別の方向にずれている可能性があります。これらの「移動」ループ割り当て句がどのように正確に機能するかを正確に覚えるのは難しいと思います。

または、より単純な「静的」loop assignsアノテーション（自分のアノテーションなど）を記述して、ループ不変条件にまだ変更されていないものに関する情報を追加することもできます。loop assignsこれは、複雑な句がどのように機能するかを思い出せないことを回避するために私が通常行うことです。それは（テストされていない）のようなものになります：

/*@
…
    loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m2)[i] == \at(((char*)m1)[i], Pre);
    loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m1)[i] == \at(((char*)m2)[i], Pre);
    loop invariant \forall integer i; (\at(n, Pre) - n) <= i < \at(n, Pre) ==> ((char*)m1)[i] == \at(((char*)m1)[i], Pre);
    loop invariant \forall integer i; (\at(n, Pre) - n) <= i < \at(n, Pre) ==> ((char*)m2)[i] == \at(((char*)m2)[i], Pre);
    loop assigns n, tmp, ((char*)m1)[0..\at(n,Pre)-1], ((char*)um2)[0..\at(n, Pre)-1], p, q;
…
@*/
于 2013-03-23T20:13:21.613 に答える