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

в моей программе есть предикат 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, может быть, если это не устарело?


verification z3 dafny
person Amir-Mousavi    schedule 24.05.2018    source источник
comment
Лучше в каком смысле?   -  person Theodore Norvell    schedule 24.05.2018
comment
@Theodore короче, и если есть какое-либо зарезервированное ключевое слово или метод, специфичный для этого   -  person Amir-Mousavi    schedule 24.05.2018

Ответы (1)


arrow_upward
2
arrow_downward

В Dafny нет встроенного понятия «не содержит дубликатов».

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

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

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

person James Wilcox    schedule 24.05.2018
comment
Спасибо. мне было интересно, можете ли вы помочь мне с этим вопросом тоже stackoverflow.com/questions/50514653/ - person Amir-Mousavi; 24.05.2018