arrays - Dafny:将 "forall"量词与 "reads"或 "modifies"子句一起使用

Question

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

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

以及包含“顶点”数组的“图形”对象:

    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 在边界内”。