あなたはすでに証明済みです。あなたは、あなたが望むプロパティを関数の事後条件として書いて、Dafnyはそれを苦情なしで検証します。それでおしまい。
また、見出しを使用してプロパティを証明することもできます。ここでは例を示します。
function count(a: seq<bool>): nat
{
if |a| == 0 then 0 else
(if a[0] then 1 else 0) + count(a[1..])
}
lemma CountProperty(a: seq<bool>)
ensures count(a) <= |a|
{
}
を繰り返しますが、あなたがそれを証明しているようDafnyは、苦情を発行せずに補題を検証します!
Dafnyが常に自動的に物事を証明すると仮定するのは間違いです。したがって、証明書を手作業で書く方法を学ぶことも良い考えです。ここに、このプロパティの手作業による証明があります。念Dafnyが自動的に誘導をしようとしません作るために、私は(これDafnyが通常と比べて、私たちの生活が困難になって)、それをオフにするディレクティブを使用:このような証明を書くため
lemma {:induction false} CountProperty(a: seq<bool>)
ensures count(a) <= |a|
{
// Let's consider two cases, just like the definition of "count"
// considers two cases.
if |a| == 0 {
// In this case, we have:
assert count(a) == 0 && |a| == 0;
// so the postcondition follows easily.
} else {
// By the definition of "count", we have:
assert count(a) == (if a[0] then 1 else 0) + count(a[1..]);
// We know an upper bound on the first term of the addition:
assert (if a[0] then 1 else 0) <= 1;
// We can also obtain an upper bound on the second term by
// calling the lemma recursively. We do that here:
CountProperty(a[1..]);
// The call we just did gives us the following property:
assert count(a[1..]) <= |a[1..]|;
// Putting these two upper bounds together, we have:
assert count(a) <= 1 + |a[1..]|;
// We're almost done. We just need to relate |a[1..]| to |a|.
// This is easy:
assert |a[1..]| == |a| - 1;
// By the last two assertions, we now have:
assert count(a) <= 1 + |a| - 1;
// which is the postcondition we have to prove.
}
}
よりよい方法Dafnyが「calc文」と呼ばれる検証済みの計算を使用することです。
lemma {:induction false} CountProperty(a: seq<bool>)
ensures count(a) <= |a|
{
if |a| == 0 {
// trivial
} else {
calc {
count(a);
== // def. count
(if a[0] then 1 else 0) + count(a[1..]);
<= // left term is bounded by 1
1 + count(a[1..]);
<= { CountProperty(a[1..]); } // induction hypothesis gives a bound for the right term
1 + |a[1..]|;
== { assert |a[1..]| == |a| - 1; }
|a|;
}
}
}
これはあなたが始めることを願っています。
安全プログラム、
Rustan