4

I am trying to prove correctness / incorrectness of the following program using 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 successfully proves that the assertion is incorrect. However it does not give an example for which the assertion has failed. Can Dafny give such an example on its own?

ankitrokdeonsns
  • 638
  • 4
  • 18

2 Answers2

4

There is a plugin for visual studio code now: https://marketplace.visualstudio.com/items?itemName=FunctionalCorrectness.dafny-vscode

You can press F7 to show counter examples, but it is not very readable for your example:

Dafny Screenshot

On the commandline you can use the mv option: Dafny.exe -mv:model.bvd myfile.dfy. This will store the model in a file named model.bvd, but it is even harder to read than the screenshot above (the plugin seems to do some postprocessing).

Peter Zeller
  • 2,245
  • 19
  • 23
2

If you run Dafny in the visual studio extension a red dot will appear next to the failed assertion. If you click the red dot then the verification debugging view should appear. This should show a counter example (which is an execution trace with variable valuations).

lexicalscope
  • 7,158
  • 6
  • 37
  • 57
  • I see a similar indicator on web version of Dafny. I dont have access to visual studio. Does command line version of Dafny show something similar? – ankitrokdeonsns Oct 02 '16 at 15:49
  • As far as I know it is not currently supported. It might be worth asking your question again at the Dafny codeplex page. – lexicalscope Oct 03 '16 at 14:41