Search code examples
z3verificationdafny

Dafny, no duplicates in an array

in my program I have a sorted predicate.

forall i,j :: 0<=i<j<a.Length ==> a[i]<a[j]

I think just checking < rather than <= avoids duplications in the array but anyhow I want to have a predicate that avoids duplications. I have used the sorted predicate but checking for non-equality

forall i,j :: 0<=i<j<a.Length ==> a[i]!=a[j]

is there a better way to do that, by other keywords in or exist or match maybe if it is not deprecated?

Solution

  • There is no builtin notion of "does not contain duplicates" in Dafny.

    I think your way of expressing it is perfectly good. Another (longer, equivalent, but maybe slightly clearer) way would be 

    forall i, j | 0 <= i < a.Length && 0 <= j < a.Length && i != j :: a[i] != a[j]

    Dafny easily shows that the two ways of writing it are equivalent.