2

こんにちは、自動控除と検証ハッカー！

WhyML が ACSL アノテーション付き C プログラムの証明をどのように正確に提供するかをより深く理解するために、Why3 が WhyML プログラムで行う作業を手動で「再現」し、それを SMT ロジックに変換して Z3 証明者にフィードしようとしています。

次の C フラグメントがあるとします。

const int L = 3;
int a[L] = {0};
int i = 0;
while (i < L) {
  a[i] = i;
  i++;
}
assert (a[1] == 1);

次のように SMT ロジックにエンコードしようとしています。

(set-logic AUFNIRA)
(define-sort _array () (Array Int Int))
(declare-const ar _array)
(declare-fun set_a_i (_array Int Int) _array)
(assert (forall ((ar0 _array) (i Int) (j Int)) 
    (ite (< i j)   
                 (= (set_a_i ar0 i j) 
                    (set_a_i (store ar0 i i) (+ i 1) j))
                 (= (set_a_i ar0 i i) ar0) ))) 

(assert (= (select (set_a_i ar 0 3) 1) 1))
(check-sat)

Z3 は「不明」を返します。

これはおそらく、set_a_i 関数を指定する際に使用される数量化によるものです。しかし、それを指定する他の方法はありません。

私は次の声明を認識しています。

  • 一般に、SMT ソルバーは、配列の数量化を処理できません (または悪い方法で処理します)。
  • 事前条件と事後条件およびループ不変条件を指定すると、WhyML はそのようなプログラムを証明できます。
  • バックエンドがZ3に設定されている場合でも、なぜMLはそのようなプログラムを証明できるので、SMTソルバー自体は問題になりません.
  • WhyML は z3 smt ファイルを生成できますが、理由の 1 つは、WhyML から smt への変換が自動的に行われるため、それを理解するのは大変な労力です (たとえば、変数名を保持しません)。

WhyML、Frama-C WP プラグイン、Z3 について提供されたほぼすべての資料を読みました。また、C コードの検証に関するいくつかの論文を読みましたが、C --> SMT 変換技術に関するものは何も見つかりませんでした。

この理解を得るには、どの資料を学習すればよいですか? 命令型コードをマルチソートされた一次ロジックに変換するこの機構を説明している論文への洞察やリンクを提供していただけませんか。

コメントをいただければ幸いです。ありがとう！

がんばれ、エフゲニー。

4

1 に答える 1

3

WP 0.8 プラグイン マニュアルと論文「Why3: Shepherd Your Herd of Provers」では、注釈付きの C コードが Why ロジックに変換される方法と、Why ロジックが定理証明器の入力ロジックに変換される方法の概要を説明しています。.

WP プラグイン マニュアルのセクション 1.3 で説明されているように、Hoare のトリプルを考慮することから始めます。

{ P } stmt { Q }

これは読み取られます: 事前条件Pが成立するときはいつでも、 stmtを実行した後、事後条件Qが成立します。WP プラグインは、次の Hoare トリプルが成立するように、stmtおよび事後条件に対する関数として最も弱い前提条件を考慮します。

{ wp ( stmt , Q )} stmt { Q }

最も弱い前提条件は、ある意味では、Qがstmtの実行後に保持されるように、 stmtの実行前に保持する必要がある最も単純なプロパティです。

例として、 stmtがx = x + 1{ Q } が {x > 0}の場合を考えてみましょう。x = x + 1ホア計算の代入則により、{x + 1 > 0} {x > 0} が成り立つことがわかっています。実際、{x + 1 > 0} はx = x + 1and {x > 0} の最も弱い前提条件です。

より一般的には、ステートメントと事後条件の最も弱い事前条件を決定することができます。

ここで、事前条件Pと事後条件Qで注釈が付けられた関数fがあるとします。

{ P } f { Q }

W = wp ( f , Q )を定義します。wpの定義により、次の Hoare トリプルが成り立つことがわかっています。

{ W } f { Q }

P ⇒ Wを証明できれば(これが定理証明者に提出されます)、fに対するプロパティPとQの有効性が確立されます。

WP プラグインは Why ロジックを生成します。「Why3: Shepherd Your Herd of Provers」ペーパーのセクション 4 で説明されているように、Why3 の操作は証明タスクの処理として説明されています。証明タスクは、ゴールで終わる一連の宣言です。これは、Why ロジックが特定の定理証明者の入力ロジックに変換される方法です。

具体的な例として、ホワイト ペーパーでは、Why ロジックを Z3 に変換する概要を説明しています。入力言語が異なるだけでなく (Z3 はSMT-LIB2構文を使用)、Why と Z3 のロジックにも大きな違いがあります。この論文では、Z3 がポリモーフィズムまたは帰納的述語をサポートしていない例を挙げています。

Why ロジックを定理証明者の入力ロジックに変換するために、Why3 は、Why ロジックを目的の入力ロジックに徐々に変換する一連の変換を使用します。Why3 は、ドライバーと呼ばれる構成ファイルを使用して、すべての変換、証明者のネイティブ入力形式を出力するプリティ プリンター、および証明者の出力を解釈するための正規表現を定義します。

を実行したと仮定すると、ホーム ディレクトリでwhy3config自動生成された構成.why3.confファイルを調べて、Why3 が特定の証明者に使用するドライバーを特定できます。たとえば、私のシステムでは~/.opam/system/share/why3/drivers/z3_432.drv、Z3 を使用するときに Why3 を使用します。 SMT-LIB2 互換の証明器のベース ドライバーとしてドライバーをz3_432.drvインポートします。smt-libv2.drv

生成された SMT2 を調べていることを知っていることは知っていますが、興味のある人のためにこれを行う方法について言及したいと思います。-wp-out DIRと-wp-proof-traceオプションを に渡すとframa-c、WP は個々のプロパティでプルーバーを実行して出力を保存します。.err次に、対象のプロパティに対応するファイルを見つけることができます。私の場合、main_assert_final_a_Why3_z3.errです。そのファイルをテキスト エディターで開くと、次のように表示されます。

Call_provers: コマンドは次のとおりです: /Users/dtrebbien/.opam/system/lib/why3/why3-cpulimit
  10 1000 -s z3 -smt2 sat.random_seed=42 nlsat.randomize=false
  smt.random_seed=42
  /var/folders/1v/2nkqhkgx0qnfwd75h0p3fcsc0000gn/T/why_9f8a52_main_Why3_ide-T-WP.smt2

この.smt2ファイルには、Why3 が生成した Z3 への SMT-LIB2 入力が含まれています。

必要に応じてコマンドを実行できます。私の場合、次のように表示されます。

警告: pattern には変数が含まれています。
警告: pattern には変数が含まれています。
警告: pattern には変数が含まれています。
警告: pattern には変数が含まれています。
未熟
Why3cpulimit 時間: 0.020000 秒

少し直感に反しunsatますが、プロパティの有効性が確立されていることを意味します。

于 2015-07-22T11:57:52.057 に答える