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的文件中，但它比上面的屏幕截图更难读（该插件似乎做了一些后处​​理）。