2

次の C コードがあるとします。

int my_main(int x){
    if (x > 5){
        x++;
        if (x > 8){
            x++;
            if (x < 15){
                //@(x >= 9 && x <= 14);
            }
        }   
    }
    return 0;
}

初期化時に変数 x の境界を静的分析を使用して計算したいと思います。これにより、満足のいく述語が得られます。この例では、メインの開始時の x の間隔は [8, 12] である必要があります。

TL;DR:コードのどこかにアサーションがある場合、これらの範囲を計算する最良の方法は何ですか?

私がこれまでに試したこと：

これにアプローチする最善の方法は、最も弱い前提条件計算機を使用することだと思います。私は frama-c の wp プラグインをいじってみましたが、検証目的で構築されているため、このユース ケースでどれほど役立つかはわかりません。次のコードにプラグインを適用する場合:

int main(void){
    int n = 0;
    int x;

    if (x > 5){
        x++;
        if (x > 8){
            x++;
            if (x < 15){
                n = x;
            }
        }   
    }
    //@ assert p: n >= 9 && n <= 14;
    return 0;
}

次の述語が代替エルゴ ソルバーに送信されます。

  goal main_assert_p:
    forall i_1,i : int.
    is_sint32(i) ->
    is_sint32(i_1) ->
    (((i < 6) -> (0 = i_1)) and
     (**(6 <= i)** ->
      (((i < 8) -> (0 = i_1)) and
       (**(8 <= i)** ->
        (((12 < i) -> (0 = i_1)) and (**(i <= 12)** -> (i_1 = (2 + i)))))))) ->
    ((9 <= i_1) and (i_1 <= 14))

注意深く見ると、結果が (i_1 = 0) にならない変数 i の境界に従うことで、入力に必要な間隔を識別することができます。私はこれらの境界をマークしました。これはあまり堅牢ではありません。たとえば、アサーションが&& n <= 13に変更された場合、暗黙の述語の「左側」は変更された条件がないため同じままです。また、関数を呼び出すときにアサーションをrequireステートメントに変更するなど、他のシナリオでこれがどれほど役立つかはわかりませんが、結果の述語を理解できません:

if (x < 15){
      sum(x);
}

そして、require ステートメントを関数に追加します。

//@requires (n >= 6 && n <= 11);
int sum(int n){

私は得る：

    goal main_call_sum_pre:
  forall i : int.
  (6 <= i) ->
  (8 <= i) ->
  (i <= 12) ->
  is_sint32(i) ->
  is_sint32(1 + i) ->
  is_sint32(2 + i) ->
  ((4 <= i) and (i <= 9))
4

2 に答える 2

3

「最も弱い前提条件」パラダイムに基づいている WP (または Jessie) が、ここで使用する適切なツールであることは間違いありません。ただし、彼らが行うことは、含意を構築することです。

仕様によって与えられた前提条件 ==> 計算された最も弱い前提条件

次に、外部の証明者は、(一般的なケースでは) 真/偽/タイムアウトの回答のみを提供して、上記の含意を証明しようとします。

user_input(*) の事後条件として「LOWER_BOUND ≤ x ≤ UPPER_BOUND」を使用し、その含意が証明されるかどうかを試行錯誤して行うことができます。ブラックボックスとして持っているツールを使用すると、二分法によって数ステップで間隔に到達します。最適な間隔があるかどうか、または証明者がまだ保持されているプロパティを証明できなくなっただけかどうかはわかりませんが、それは人生です。

または、単純化作業を証明者に任せることもできますが、それには、単に「このプロパティは真か?」よりも複雑な対話が必要です。一部の証明者は、他の証明者よりも簡単にその情報にアクセスできるようにします。本当に、WPがその仕事をした後、それはすべて証明者の手にあります。あなたの質問は、xFrama-Cについてではなく、「論理式を境界に縮小して式を真にする証明者」に関するものです。

この研究には、いくつかの場所で「あなたができる最善の間隔を教えてください」という質問が含まれていました. これは浮動小数点に関するものですが、浮動小数点は整数よりも推論が難しいだけであるため、そこで使用されるツールと手法は問題にも適用される可能性があります。特に、浮動小数点を専門とする「Gappa」証明者は、間隔でネイティブに動作し、IIRC は、その調査で必要に応じて「最良の」間隔を提供した証明者でした (たとえば、11 ページ、「どのように私たちは私たちの例示的な例では、境界 1/16 を決定しますか?」)

(*)user_input()意味を明確にするために への呼び出しを追加した後、実際に探しているのは、メイン関数の事前条件ではなく、その関数の事後条件であることに注意してください。

于 2016-02-09T10:40:42.750 に答える
-1

assertはブール式を取り、 の場合FALSE、メッセージを表示してアプリケーションを中止します。assertは通常マクロであり、プログラムの非デバッグ バージョンでは、これらのマクロの呼び出しは前処理中に削除されます。

ブール式に定数が含まれています。それらを変数に置き換えると、柔軟なアサートができます。

于 2016-02-09T10:29:15.343 に答える