Дафни, без дубликатов в массиве

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

В Дафни нет встроенного понятия "не содержит дубликатов".

Я думаю, что ваш способ выразить это совершенно хорошо.Другой (более длинный, эквивалентный, но, возможно, немного более ясный) способ будет

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

Дафни легко показывает, что два способа написания этого текста эквивалентны.