-1

C で strlen のような関数を証明しようとしていますが、frama-c は事後条件とloop variant len節を証明しません。理由がわかりません！

私が試したこと：

/*@
    axiomatic elementNumber_axioms
    {
        logic unsigned elementNumber{L}(char *a);

        axiom elementNumber_base{L}:
            elementNumber(\null) == 0;

        axiom elementNumber_step{L}:
            \forall char *a;
            \valid(a) ==> elementNumber(a) == elementNumber(a+1) + 1;
    }
*/

/*@
    assigns \nothing;
    ensures \result == elementNumber(\old(s));
*/
unsigned stringlen(const char *s)
{
    unsigned len = 0;

/*@
    loop assigns len;
    loop assigns s;
    loop variant len;
*/
    while(*s)
    {
        ++s;
        ++len;
    }

    return len;
}

私は何を間違っていますか？

4

1 に答える 1

3

あなたが書いたものにはいくつかの問題があります。網羅的でないリスト:

  • stringlen()sは NULL のケースを処理しません。

    標準 C の strlen() 関数に注釈を付ける場合、標準 C の strlen() 関数ではパラメーターを にすることができないため、このケースを処理する必要はありませんNULL。ただし、 elementNumber() 論理関数の公理的定義はelementNumber(\null)0 であると定義しており、stringlen() の事後条件は結果が等しいことですelementNumber(s)。したがって、このケースを処理する必要があります。

  • stringlen() の while ループは、nul バイトに遭遇すると終了します。ただし、 elementNumber() ロジック関数の定義は、ポインターが有効かどうかのみに依存します。

  • 、 などが有効かどうかについてs、stringlen() には前提条件はありません。s + 1

  • elementNumber() ロジック関数は、無効なポインターの値を定義していません。

  • ループ不変条件を指定する必要があります。

Frama-C が strlen() にどのように注釈を付けるかを確認することをお勧めします。

/*@ requires valid_string_src: valid_string(s);
  @ assigns \result \from s[0..];
  @ ensures \result == strlen(s);
  @*/
extern size_t strlen (const char *s);

strlen() 論理関数と valid_string() 述語はshare/libc/__fc_string_axiomatic.h、この記事の執筆時点で Sodium-20150201 であるソース配布で定義されています。

于 2015-07-21T22:10:48.470 に答える