dafny可以顯示一個失敗斷言的反例嗎？

Question

我想證明使用Dafny的以下程序的正確性/不正確性。

datatype List<T> = Nil | Cons(T, List) 
function tail(l:List):List 
{ 
    match l 
    case Nil => Nil 
    case Cons(x,xs) => xs 
} 
method check(l:List) 
{ 
    assert(expr(l)!=2); 
} 
function expr(l : List):int 
{ 
    if(l == Nil) then 0 
    else if(tail(l)==Nil) then 1 
    else if(tail(tail(l)) == Nil) then 2 
    else 3 
} 

Dafny成功地證明斷言是不正確的。 但是它沒有給出斷言失敗的例子。戴夫尼可以自己舉這樣一個例子嗎？

Answer 1

如果在Visual Studio擴展中運行Dafny，失敗的斷言旁邊將出現一個紅點。如果您單擊紅色圓點，則應顯示驗證調試視圖。這應該顯示一個反例（這是一個變量估值的執行軌跡）。

Answer 2

沒有爲Visual Studio代碼插件現在：https://marketplace.visualstudio.com/items?itemName=FunctionalCorrectness.dafny-vscode

您可以按F7顯示反例，但它不是你的例子非常可讀的：

在命令行您可以使用mv選項：Dafny.exe -mv:model.bvd myfile.dfy。這會將模型存儲在一個名爲model.bvd的文件中，但它比上面的屏幕截圖更難讀（該插件似乎做了一些後處​​理）。