assertion violation when verifying Max function in Dafny?

Question

The following program results in an assertion violation on assert v==40: why ? The program can be verified when the array a contains only one element.

method Max(a:array<int>) returns(max:int)
requires 1<=a.Length
ensures forall j:int :: 0<=j< a.Length ==> max >= a[j]
ensures exists j:int :: 0<=j< a.Length &&  max == a[j]
{
   max:=a[0];
   var i :=1;
   while(i < a.Length)
   invariant 1<=i<=a.Length
   decreases a.Length-i
   invariant forall j:int :: 0<=j<i ==> max >= a[j]
   invariant exists j:int :: 0<=j<i &&  max == a[j]
   {
     if(a[i] >= max){max := a[i];}
     i := i + 1;
   }
}
method Test(){
   var a := new int[2];
   a[0],a[1] := 40,10;
   var v:int:=Max(a);
   assert v==40;
}

James Wilcox James Wilcox · Accepted Answer · 2018-04-30T15:46:16

This is indeed strange! It boils down to the way Dafny handles quantifiers.

Let's start with a human-level proof that the assertion is actually valid. From the postconditions of Max, we know two things about v: (1) it is at least as big as every element in a, and (2) it is equal to some element of a. By (2), v is either 40 or 10, and by (1), v is at least 40 (because it's at least as big as a[0], which is 40). Since 10 is not at least 40, v can't be 10, so it must be 40.

Now, why does Dafny fail to understand this automatically? It's because of the forall quantifier in (1). Dafny (really Z3) internally uses "triggers" to approximate the behavior of universal quantifiers. (Without any approximation, reasoning with quantifiers is undecidable in general, so some restriction like this is required.) The way triggers work is that for each quantifier in the program, a syntactic pattern called the trigger is inferred. Then, that quantifier is completely ignored unless the trigger matches some expression in the context.

In this example, fact (1) will have a trigger of a[j]. (You can see what triggers are inferred in Visual Studio or VSCode or emacs by hovering over the quantifier. Or on the command line, by passing the option /printTooltips and looking for the line number.) That means that the quantifier will be ignored unless there is some expression of the form a[foo] in the context, for any expression foo. Then (1) will be instantiated with foo for j, and we'll learn max >= a[foo].

Since your Test method's assertion doesn't mention any expression of the form a[foo], Dafny will not be able to use fact (1) at all, which results in the spurious assertion violation.

One way to fix your Test method is add the assertion

assert v >= a[0];

just before the other assertion. This is the key consequence of fact (1) that we needed in our human level proof, and it contains the expression a[0], which matches the trigger, allowing Dafny to instantiate the quantifier. The rest of the proof then goes through automatically.

For more information about triggers in general and how to write them manually, see this answer.

assertion violation when verifying Max function in Dafny?

1 Answers