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 扩展中运行 Dafny，失败的断言旁边会出现一个红点。如果单击红点，则应出现验证调试 View 。这应该显示一个反例(这是一个具有可变估值的执行跟踪)。