
I am new to Dafny. I have two questions to begin with.
 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.
 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 5:19 AM
Edited May 15, 2016 at 5: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.



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.



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.



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.



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.

