Dafny遞歸斷言違規

我是dafny的新手，我試圖讓這段簡單的代碼工作。我想計算字符串中char的出現次數。我在第4行收到斷言違規。我知道我的功能是找到適量的字符，但顯然這個斷言存在一些漏洞。我試圖在開始使用事前和事後條件之前弄清楚基礎知識，並且沒有這些基礎知識，而且如果沒有它們，這應該是可能的。該函數簡單地檢查字符串中的最後一個字符並返回1或0，並再次調用該函數以切斷字符串的尾部，直到它爲空。Dafny遞歸斷言違規

method Main() { 
    var s:string := "hello world"; 
    print tally(s, 'l'); 
    assert tally(s,'l') == 3; 
} 
function method tally(s: string, letter: char): nat 
{ 
    if |s| == 0 then 0 
    else if s[|s|-1] == letter then 1+tally(s[..|s|-1], letter) 
    else 0 + tally(s[..|s|-1], letter) 
}

http://rise4fun.com/Dafny/2lvt 這裏是鏈接到我的代碼。

來源

2017-06-02 Andrew McMenemy

認爲Dafny靜態驗證器可以評估任何代碼，比如assert語句中的表達式，這是很自然的。驗證器確實嘗試評估這些表達式，其中參數作爲常量給出（如您的"hello world"，'l', 和3）。然而，靜態驗證者想要永遠避免遞歸（或者甚至遞歸太長時間），所以它並不總是完全通過這些表達式來通過。在你的情況下，也有限制，驗證者能夠處理序列操作。所以，在之後，儘管驗證者試圖有幫助，但並不總是到達遞歸的底部。

有兩種方法可以解決這些限制，讓驗證程序接受您的斷言。

調試情況的最可靠的方法是從較小的輸入開始，建立到您使用的較長輸入。然而，這是相當乏味的，當Dafny能夠自動執行這些事情時，它會讓你感激不盡。（該驗證）以下說明你會做什麼：

var s := "hello world"; 
assert tally("he",'l') == 0; 
assert tally("hel",'l') == 1; 
assert "hell"[..3] == "hel"; 
assert tally("hell",'l') == 2; 
assert "hello"[..4] == "hell"; 
assert tally("hello",'l') == 2; 
assert "hello "[..5] == "hello"; 
assert tally("hello ",'l') == 2; 
assert "hello w"[..6] == "hello "; 
assert tally("hello w",'l') == 2; 
assert "hello wo"[..7] == "hello w"; 
assert tally("hello wo",'l') == 2; 
assert "hello wor"[..8] == "hello wo"; 
assert tally("hello wor",'l') == 2; 
assert "hello worl"[..9] == "hello wor"; 
assert tally("hello worl",'l') == 3; 
assert s[..10] == "hello worl"; 
assert tally(s,'l') == 3;

事實上，事情的Dafny驗證不擴大（太多倍），在你的「拿」操作（即，的表達式s[..E]）。以下中間斷言也將驗證自己並有助於驗證最終斷言。這些中間斷言顯示驗證者不認爲自動爲您執行。

var s := "hello world"; 
assert "he"[..1] == "h"; 
assert "hel"[..2] == "he"; 
assert "hell"[..3] == "hel"; 
assert "hello"[..4] == "hell"; 
assert "hello "[..5] == "hello"; 
assert "hello w"[..6] == "hello "; 
assert "hello wo"[..7] == "hello w"; 
assert "hello wor"[..8] == "hello wo"; 
assert "hello worl"[..9] == "hello wor"; 
assert s[..10] == "hello worl"; 
assert tally(s,'l') == 3;

你可能不知道，「如何在世界上我會想出這個？」。最有系統的方法是從上面的第一個例子開始。然後，你可以嘗試修剪那裏的許多斷言，看看它是什麼是驗證者的需要。

（我現在想，或許Dafny驗證，可以增強做這些操作了。這可能會導致性能問題在其他地方。我會看看。）

的另一種方式工作圍繞驗證者的限制是以不同的方式定義函數tally，特別是避免驗證者不希望擴大的「操作」操作。這是不清楚什麼改變，使驗證這些情況快樂，或者如果這甚至有可能在所有的，所以這種替代方法可能不是最好的。不過，我試過的 tally以下定義，它使你的主張經過：

function method tally'(s: string, letter: char): nat 
{ 
    tally_from(s, letter, 0) 
} 
function method tally_from(s: string, letter: char, start: nat): nat 
    requires start <= |s| 
    decreases |s| - start 
{ 
    if start == |s| then 0 
    else (if s[start] == letter then 1 else 0) + tally_from(s, letter, start+1) 
}

注意，這些定義不使用任何「吃」的操作。在這裏，驗證是幸福的，直到最後答案被發現展開所有的遞歸調用。

Rustan

來源

2017-06-06 01:43:06

非常深入的感謝您的幫助！ –

Dafny遞歸斷言違規

回答

相關問題