Блог

Я пытаюсь доказать правильность / некорректность следующей программы, используя 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 привести такой пример сам по себе?

Теперь есть плагин для кода Visual Studio: https://marketplace.visualstudio.com/items?itemName=FunctionalCorrectness .dafny-vscode

Вы можете нажать F7 , чтобы показать встречные примеры, но это не очень удобно для вашего примера:

В командной строке вы можете использовать mv опцию: Dafny.exe -mv:model.bvd myfile.dfy . Это сохранит модель в файле с именем model.bvd , но его еще сложнее прочитать, чем на скриншоте выше (плагин, похоже, выполняет некоторую постобработку).

Если вы запустите Dafny в расширении Visual Studio, рядом с неудачным утверждением появится красная точка. Если щелкнуть красную точку, должно появиться представление отладки проверки. Это должно показать встречный пример (который представляет собой трассировку выполнения с оценками переменных).