dafny 可以举一个失败断言的反例吗？答案

【问题标题】：Can dafny show a counter example for a failed assertion?dafny 可以举一个失败断言的反例吗？
【发布时间】：2017-02-10 09:24:24
【问题描述】：

我正在尝试使用 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 可以自己举一个这样的例子吗？

【问题讨论】：

标签： verification dafny

【解决方案1】：

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

【讨论】：

我在网络版 Dafny 上看到了类似的指标。我无法访问视觉工作室。 Dafny 的命令行版本是否显示类似的内容？
据我所知，目前不支持。在 Dafny codeplex 页面上再次询问您的问题可能是值得的。

【解决方案2】：

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

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

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

【讨论】：