verification - 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 成功地证明了断言是不正确的。然而，它没有给出断言失败的例子。Dafny 可以自己举一个这样的例子吗？

Answer 1

现在有一个 Visual Studio 代码插件：https ://marketplace.visualstudio.com/items?itemName=FunctionalCorrectness.dafny-vscode

您可以按F7显示反例，但对于您的示例来说，它的可读性不是很高：

在命令行上，您可以使用mv选项：Dafny.exe -mv:model.bvd myfile.dfy. 这会将模型存储在一个名为 的文件中model.bvd，但它比上面的屏幕截图更难阅读（插件似乎做了一些后处​​理）。

Answer 2

如果您在 Visual Studio 扩展程序中运行 Dafny，则失败的断言旁边会出现一个红点。如果单击红点，则应出现验证调试视图。这应该显示一个反例（这是一个具有可变估值的执行跟踪）。