2

私は現在、楽しいプロジェクトとして Z3 の上に自分のプログラミング言語用の自動検証ツールを書いています。これを使用して、ループを使用したフィボナッチ実装が再帰を使用したものと同等であることを証明しようとしています。

入力プログラムが正しい場合、つまり、Z3 に対して適切な入力を生成し、Z3 が満足できないと言う場合、これは私のコンテキストではプログラムが正しいことを意味します。しかし、変数の初期化を 1 つ変更したためにプログラムが正しく表示されなくなったとき、検証者は次の Z3 式を思いつきました。これは私にはそれほど複雑ではないように見えますが、Z3 は「不明」と言っています。

(set-option :smt.auto-config false)
(set-option :smt.mbqi false)
(declare-fun fib (Int) Int)
(declare-fun fakeFib (Int) Int)
(declare-fun n () Int)
(assert (forall ((n Int))
   (! (= (fib n)
         (ite (= n 0) 0
            (ite (= n 1) 1
               (+ (fakeFib (- n 1)) (fakeFib (- n 2))))))
      :pattern ((fib n)))))
(assert (forall ((n Int))
   (! (= (fib n) (fakeFib n)) :pattern ((fib n)))))
(assert (>= n 0))
(assert (not (and (<= 0 n) (= 1 (fib 1)) (= 1 (fib 0)))))
(check-sat)

2 つの量指定子は、フィボナッチの再帰的な定義を表していることに注意してください。私の友人は、一致するループを回避するためのこのトリックを教えてくれました: fib を再帰関数として定義する代わりに、定義を提供しない別の関数 fakeFib を導入し、それを fib の再帰定義で使用します。また、検証者にそれらが等しいことを伝えますが、その量指定子は fib のパターンのみを取得し、fakeFib のパターンは取得しません。つまり、プログラムの正しさを証明するには、1 レベルの再帰を見るだけで十分です (ただし、k レベルに簡単に拡張できます)。しかし、ループの一致を避けるために、その制限に耐えることができます。

コードの「バグ」は、変数を誤って初期化したことであり、これが最終的(= 1 (fib 0))に最後のアサーションで誤ったコンポーネントにつながりました。正しいプログラムの場合、それは(= 0 (fib 0)).

いくつかの観察：

  • で置き換える(= 1 (fib 0))と(= 0 (fib 0))、Z3 はそれが満足できないことをすぐに判断します。
  • 以前は、オプション(set-option :smt.auto-config false)と(set-option :smt.mbqi false)設定がなく、マシンのメモリが不足し、rise4fun の時間が不足していました。
  • (set-option :smt.macro-finder true)同様の質問を持つ人々にとってうまくいったと思われる設定は、私にはうまくいきませんでした。これは、1 つだけでなく2 つの量指定子があることが原因であると推測していfibます。
  • 比較としてcvc4を使用してみましたが、すぐに「不明」と表示されました。したがって、私の問題は Z3 固有のものではないようです。
  • 式は明らかに充足可能です。(= 1 (fib 0))であるfalseため、最後のアサーション全体が自動的に true になります。(>= n 0)も満足しやすい。
4

1 に答える 1