Есть ли способ прочитать поля массива объектов класса в dafny

Question

Скажем, у меня был класс Player в dafny с полем под названием Score, по которому я хочу отсортировать. Есть ли способ в dafny, где я мог бы получить доступ к полям класса за пределами класса. Это фрагмент:

predicate PlayersSorted(a: array<Player>)
reads a
{
  forall j, k :: 0 <= j < k < a.Length ==> a[j].score <= a[k].score
}

Это выдает ошибку insufficient reads clause to read field при попытке получить доступ к полю оценки, но я не могу найти предложение чтения, которое позволило бы мне сделать это в руководстве. Если это невозможно, может кто-нибудь предложить предложение о том, как вы будете проверять сортировку по классу, подобному объекту.

Answer 1

Вам необходимо добавить предложение reads для элементов массива, например reads set x | x in a[..].

. В дальнейшем вам также может потребоваться заглянуть в главу 9 (Динамические кадры) из http://leino.science/papers/krml221.pdf для некоторых идиом при работе с предложениями modifies / reads.