Как использовать предложение «reads» для чтения массива последовательностей в Dafny?

Question

В моей реализации кода у меня есть массив последовательностей с элементами кортежа (int, string), который int представляет ключ и string значение.

Я пытаюсь выполнить sh следующая проверка «Не должно быть повторяющегося ключа во всех элементах, присутствующих в массивах».

У меня есть следующий код, но у меня возникают проблемы при чтении элементов последовательности.

var buckets:array<seq<(int, string)>>;

function Valid():bool 
    reads `buckets //set x | x in buckets[..] Broken attempt that tries to read the elements
{ 
    buckets.Length > 0 
    // Some code just to try to read the sequence elements
    // && forall i :: 0 <= i < buckets.Length ==> forall j :: 0 <= j < |buckets[i]| ==> buckets[i][j].0 != buckets[i][j].0
} 

Какие-нибудь советы о том, как я могу преодолеть эту проблему?

Answer 1

Функция должна объявлять набор объектов, состояние которых она читает. Массив - это объект. Я предполагаю, что ваш фрагмент кода выше находится внутри класса.

• Ваша функция читает поле buckets this, поэтому вам нужно включить this в reads clause.

  Вы сделали это расширенным способом, который говорит, что функция зависит от this, но только от поля buckets this. Если вам действительно нужна эта точность, вы делаете это правильно. Если вам не нужна эта точность, я предлагаю заменить

  reads `buckets
  

  на

  reads this
  

• Ваша функция читает поле Length поля this.buckets. Однако Length является полем только для чтения, поэтому вам не нужно указывать this.buckets в рамке чтения.

• Ваша функция читает buckets[i]. То есть он читает элемент i из this.buckets. Следовательно, вы должны включить this.buckets в ваше предложение reads.

Итак, сделайте это:

reads this, buckets

и ваша функция проверит.