Dafny，数组中没有重复项

Question

在我的程序中，我有一个sorted谓词。

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

我认为只检查<而不是<=可以避免数组中的重复，但无论如何，我想要一个避免重复的谓词。 我使用了排序的谓词，但检查不相等

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

有没有更好的方法来做到这一点，通过其他关键字in或exist或match，如果它没有被弃用？

Answer 1

Dafny中没有"不包含重复项"的内置概念。

我认为你的表达方式非常好。另一种(更长，等效，但可能更清晰(的方式是

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

Dafny很容易证明这两种写法是等价的。