Some issues with Dafny

May 14, 2016 at 5:12 PM
I am new to Dafny. I have two questions to begin with.
  1. Where is the output of a compiled program in Dafny in Visual Studio? I have "print" statement and a return statement but can see no output.
  2. Why do I get assertion violation for the following simple program?
    method main() returns(i:int)
    var a: array<int> := new int[4];
    a[0], a[1], a[2], a[3] := 1, 2, 3, 4;
    assert exists i :: 0 <= i < a.Length && a[i] == 3;
    print "hello, Dafny\n";
    return a[3];
May 15, 2016 at 4:19 AM
Edited May 15, 2016 at 4:21 AM
For the second question, Dafny usually doesn't prove existential assertion automatically.
You have to assist it by providing a concrete witness or an inductive proof.
In your example, inserting assert a[2] == 3; before the existential assertion will do the job.
May 15, 2016 at 5:38 AM
Thanks. Yes I knew that works. But the funny thing is with the existing code if I change the "assert" so as to assert about the last element of the array it works! Moreover it is not even able to verify
assert exists i : nat :: 0<= i < a.Length
for the array a.

May 15, 2016 at 1:13 PM
As I said, Dafny needs hints to prove even the simplest assertion when it comes to existential quantifiers.
It can not even show assert exists i: int :: i == 0 without a hint.

Besides, assertions like assert exists i: int :: i == 0 (as well as assert exists i: nat :: 0 <= i < a.Length) would produce a "No terms found to trigger on" error. You may get around this error by wrapping your condition in a predicate (e.g., define eq for integers and write eq(i, 0) instead of i == 0). For more details, please see this post and the reference therein.
May 15, 2016 at 3:08 PM
Thanks again. But I am curious about the fact it does not complain if one asserts about the last assignment in the array. I think I tried the predicate wrapping method too. How does Dafny or rather the theorem prover behind the scene try to instantiate to prove an existential. I suppose one could construct the set (of array indices, for example) and force it to look in there. By the way, the example I gave was very similar to one in the slides Dafny: a digest. Only they used the last array assignment there.

Any thoughts on my other question about no output even when the program compiles. I had the output window open.

May 15, 2016 at 8:25 PM
Here is (part of) the boogie that is generated for the heap updates:
    $Heap := update($Heap, $obj0, $index0, $Box($rhs#0)); 
    $Heap := update($Heap, $obj1, $index1, $Box($rhs#1));
    $Heap := update($Heap, $obj2, $index2, $Box($rhs#2));
    $Heap := update($Heap, $obj3, $index3, $Box($rhs#3));
So the heap being used in the assertion is something like:
    update(update(update(update($Heap, $obj0, $index0, $Box($rhs#0)), $obj1, $index1, $Box($rhs#1)), $obj2, $index2, $Box($rhs#2)), $obj3, $index3, $Box($rhs#3));
And update is a function
   function {:inline true} update<alpha>(H: Heap, r: ref, f: Field alpha, v: alpha) : Heap
      H[r, f := v]
I suspect that boogie (Z3?) has built into its map implementation the knowledge that H[r,f := v][r,f]==v. But it is not generally the case that H[r,f := v][s,g:=w][r,f]==v since perhaps r,f == s,g, so we aren't getting help with the early updates.