z3 - 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如果它没有被弃用？existmatch

Answer 1

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

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

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

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