dafnyformal-verificationinvariantspost-conditions

Dafny Method to find Max fails to verify

I'm working on a Dafny program that finds the maximum element in a sequence of integers. The method Strictmax should return the maximum element and its index. If the maximum element is not unique, the index should be -1.

I have a predicate isUniqueMax, that I use in the postcondition and is causing problems for Dafny.

predicate isUniqueMax(s: seq<int>, max: int, idx: int)
{
  (exists i :: 0 <= i < |s| && s[i] == max) ==>
  (
    (idx != -1 ==> (forall j :: 0 <= j < |s| ==> (s[j] == max ==> j == idx))) &&
    (idx == -1 ==> exists j, k :: 0 <= j < k < |s| && s[j] == max && s[k] == max)
  )
}

method Strictmax(s:seq<int>) returns(max:int, idx:int)
  requires |s| > 0 
  ensures ismax(s, max, |s|)
  ensures isUniqueMax(s, max, idx)
{..}
 
method Validator()
{
  var s1 := [1, 42, 9];
  var max1, idx1: int;
  max1, idx1 := Strictmax(s1);
  assert max1 >= s[0];
  assert max1 == 42 && idx1 == 1;
  
  // ... (other test cases)
}

When I run the Dafny verifier, it says that the assertion in the verifier might not hold. I suspect that the issue is my postconditions (specifically isUniqueMax).

How can I modify the code to ensure that it verifies?

Solution

  • You can add this line to the Verifier method:

    assert max1 >= s1[1];

    The reason this matters is because the postcondition for StrictMax includes forall quantifiers, which Dafny reasons about via triggers. By mentioning the expression s1[1], we cause Dafny to learn that max >= 42, which, since Dafny also knows that max has to be equal to something in the array, also implies that max == 42.