有没有办法在 dafny 中读取类对象数组的字段

Question

假设我在 dafny 有一个 Player 课程，其中有一个名为 score 的字段，我想对其进行排序。在 dafny 中有没有一种方法可以让我在课堂外访问课堂的字段。这是一个sn-p：

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[..]。

接下来，您可能还想查看http://leino.science/papers/krml221.pdf 的第 9 章（动态帧），了解使用 modifies/reads 子句时的一些习语。