z3 - 正しい Dafny メソッドの Z3 モデル

Question

正しいメソッドの場合、Z3 はメソッドの検証条件のモデルを見つけることができますか?

私はそうではないと思っていましたが、これはメソッドが正しい例です

それでも、検証によってモデルが見つかります。

これは Dafny 1.9.7 で発生しました。

Answer 1

Dafny は、再帰的定義 (ここではPow) と帰納法の 2 つの不完全性の原因の組み合わせにより、補題を証明できません。情報が少なすぎるため、つまり問題が制約不足であるため、証明は事実上失敗します。これにより、反例が見つかる理由が説明されます。

誘導

帰納法の自動化は、帰納仮説を計算する必要があるため困難です。これは常に可能であるとは限りません。ただし、Dafny には誘導を適用するためのいくつかのヒューリスティック(動作する場合と動作しない場合があります) があり、次のコードのように切り替えることができます。

lemma {:induction false} EvenPowerLemma_manual(a: int, b: nat)
  requires Even(b);
  ensures Pow(a, b) == Pow(a*a, b/2);
{
  if (b != 0) {
    EvenPowerLemma_manual(a, b - 2);
  }
}

ヒューリスティックをオフにするとb >= 2、証明を得るために手動で補題を「呼び出す」必要があります。つまり、帰納仮説 (ここでは、 の場合のみ) を使用します。

あなたの場合、ヒューリスティックは有効になりましたが、証明を完了するには「十分」ではありませんでした。理由は次回に説明します。

再帰的な定義

再帰的な定義を展開して静的に推論すると、一般にいつ停止するかを決定できないため、無限降下が発生しやすくなります。したがって、デフォルトでは、Dafny は関数定義を 1 回だけ展開します。あなたの例では、帰納仮説を に適用する必要があるため、 の定義をPow1 回だけ展開するだけでは帰納ヒューリスティックを機能させるのに十分ではPow(a, b-2)ありませんPow(a, b - 1)。ただし、証明で明示的に言及Pow(a, b-2)すると、それ以外の場合は無意味な式であっても、帰納法ヒューリスティックがトリガーされます。

function Dummy(a: int): bool
{ true }

lemma EvenPowerLemma(a: int, b: nat)
  requires Even(b);
  ensures Pow(a, b) == Pow(a*a, b/2);
{
  if (b != 0) {
    assert Dummy(Pow(a, b - 2));
  }
}

このDummy関数は、アサーションが構文的に を含む以上の情報を提供しないことを確認するためにありますPow(a, b-2)。あまり奇妙に見えないアサーションは ですassert Pow(a, b) == a * a * Pow(a, b - 2)。

計算証明

参考までに: 証明の手順を明示的にして、Dafny に確認させることもできます。

lemma {:induction false} EvenPowerLemma_manual(a: int, b: nat)
  requires Even(b);
  ensures Pow(a, b) == Pow(a*a, b/2);
{
  if (b != 0) {
    calc {
         Pow(a, b);
      == a * Pow(a, b - 1);
      == a * a * Pow(a, b - 2);
      == {EvenPowerLemma_manual(a, b - 2);}
         a * a * Pow(a*a, (b-2)/2);
      == Pow(a*a, (b-2)/2 + 1);
      == Pow(a*a, b/2);
    }
  }
}