Dafny：使用带有“reads”或“modifies”子句的“forall”量词

Question

因此，作为本科项目的一部分，我正在尝试直接根据 CLRS 算法书中算法的描述，在 Dafny 中实现 Dijkstra 的单源最短路径算法。作为实现的一部分，我定义了一个“顶点”对象，其中包含两个字段，分别表示从源到前一个顶点的最短路径的当前长度：

    class Vertex{
    var wfs : int ;   
    var pred: Vertex;
    }

以及包含“顶点”-es 数组的“图形”对象：

    class Graph{
    var vertices: array<Vertex>;
    ....

我正在尝试使用“图形”对象中的谓词来声明顶点数组的每个“顶点”中字段的一些属性：

    predicate vertexIsValid() 
    reads this;
    reads this.vertices;
     {
       vertices != null &&
       vertices.Length == size &&
       forall m :: 0 <= m < vertices.Length ==> vertices[m].wfs != 900000 && 
       vertices[m].pred != null
     }

据我了解，Dafny 中的“读取”和“修改”子句仅适用于一层，我必须向 Dafny 指定我将读取顶点数组中的每个条目（读取 this.vertices[x ])。我尝试使用“forall”子句来做到这一点：

   forall m :: 0 <= m < vertices.Length ==> reads this.vertices[m]

但这似乎不是 Dafny 的功能。有谁知道是否有办法在“读取”子句中使用量词，或者告诉 Dafny 读取包含对象的数组的每个条目中的字段？

感谢您的帮助。

Answer 1

您可以使用set 作为reads 子句最轻松地做到这一点。

对于您的示例，vertexIsValid 上的附加 reads 子句对我有用：

reads set m | 0 <= m < vertices.Length :: vertices[m]

您可以将这个set 表达式视为“所有元素的集合vertices[m] 其中m 在边界内”。