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?
You can add this line to the
Verifier
method:The reason this matters is because the postcondition for
StrictMax
includesforall
quantifiers, which Dafny reasons about via triggers. By mentioning the expressions1[1]
, we cause Dafny to learn thatmax >= 42
, which, since Dafny also knows thatmax
has to be equal to something in the array, also implies thatmax == 42
.