2

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

    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 读取包含对象的数组的每个条目中的字段？

谢谢您的帮助。

4

1 回答 1

2

set使用asreads子句可以最轻松地做到这一点。

对于您的示例，此附加reads条款对vertexIsValid我有用：

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

您可以将此set表达式视为“所有元素vertices[m]的m集合”。

于 2018-01-24T19:19:56.120 回答