Dafny：在 "reads" 或 "modifies" 子句中使用 "forall" 量词

Question

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

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

以及包含 "Vertex"-es 数组的 "Graph" 对象：

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

我正在尝试使用 "Graph" 对象中的谓词来说明顶点数组的每个 "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 中的 "reads" 和 "modifies" 子句仅适用于一层，我必须向 Dafny 指定我将读取顶点数组中的每个条目（读取 this.vertices[x] ) 。我尝试使用 "forall" 子句来做到这一点：

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

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

感谢您的帮助。

Answer 1

您可以通过将 set 用作 reads 子句来最轻松地做到这一点。

以您的示例为例，vertexIsValid 上的这个附加 reads 子句对我有用：

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

您可以将此 set 表达式视为 "the set of all elements vertices[m] where m is in bounds"。

Dafny：在 "reads" 或 "modifies" 子句中使用 "forall" 量词

Dafny: Using "forall" quantifiers with the "reads" or "modifies" clauses

arrays

algorithm

formal-verification

dafny