私たちは、機能的なプログラム検証のためのリレーショナル ロジックを実験しています。私たちのロジックには、代数データ型に対する関係と、関係に対する等式およびサブセット包含述語が備わっています。私たちの検証手順は、帰納的プログラム分析 (構造帰納法) を実行し、十分に強い帰納仮説を使用して検証条件 (VC) を生成します。検証手順によって生成された VC は、次の形式に従います。
bindings <var-type bindings> in <antecedent-predicate> => <consequent-predicate> end
以下は、手順によって生成された VC の例です: http://pastebin.com/exncPHDA
このように生成された VC を、次の規則を使用して SMT2 言語でエンコードします。
- 各具象型 (例: 'a list) は、解釈されないソートに変換されます。
- リレーションは、解釈されない並べ替えから bool までの解釈されない n 項関数としてエンコードされます。
- リレーショナル アサーション (例: R = R1 U R2、R = R1 X R2) は、解釈されていない関数に対するプレネックス定量化されたアサーションとしてエンコードされます。
上記のエンコードの結果は、(おそらく) 効果的な命題 (EPR) の一次論理の式です。Z3 の助けを借りて、多くの VC の妥当性 (否定の不充足性) を主張することができました。ただし、VC が無効な場合 (否定が SAT の場合)、Z3 がループする場合があります。上記の例 ( http://pastebin.com/exncPHDA ) はそのような VC の 1 つであり、その SMT2 エンコーディングはhttp://pastebin.com/s8ezha7Dに示されています。この式をアサートしている間、Z3 は終了しないようです。
数量化されたブール式を決定することは非常に困難であることを考えると、決定手順が終了しないことはそれほど驚くべきことではありません。それにもかかわらず、非終了の可能性を最小限に抑えるために、Z3 で数式をエンコードする際に実行できる最適化があるかどうかを知りたいです。
- 現在のエンコーディングでは、多くの空のセット (つまり、forall x:T, f(x)=falseの形式の 1 つのアサーション) と、同じシングルトン セットの多くのインスタンス (つまり、forall x:T, (f(x) = true) ) が作成されます。 => (x = v) )。そのような重複を減らすことは役に立ちますか?
- プログラムの精緻化により、現在、多くの変数と推移的な等式があります。変数の数を減らすことは役に立ちますか?
また、満たされない量化されたブール式を決定する際に Z3 がループする可能性はどのくらいありますか?