ダフィーの数を証明する方法<size

Question

私は現在Dafnyを学んでいます。私は補題で完全に納得しています。私はそれをどのように使うべきか分かりません。このチュートリアルは役に立ちません。何を証明したいのですか count(a) <= |a| どうすればいいですか？助けてくれてありがとう。

function count(a: seq<bool>): nat 
ensures count(a) <= |a|; 
{ 
    if |a| == 0 then 0 else 
    (if a[0] then 1 else 0) + count(a[1..]) 
} 

Answer 1

あなたはすでに証明済みです。あなたは、あなたが望むプロパティを関数の事後条件として書いて、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