因此,作为本科生项目的一部分,我尝试直接根据 CLRS 算法书中的算法描述在 Dafny 中实现 Dijkstra 的单源最短路径算法。作为实现的一部分,我定义了一个“Vertex”对象,其中两个字段表示从源和前驱顶点开始的最短路径的当前长度:
class Vertex{
var wfs : int ;
var pred: Vertex;
}
以及包含“Vertex”数组的“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 中的“读取”和“修改”子句仅适用于一层,我必须向 Dafny 指定我将读取顶点数组中的每个条目(读取 this.vertices[x ])。我尝试使用“forall”子句来做到这一点:
forall m :: 0 <= m < vertices.Length ==> reads this.vertices[m]
但这似乎不是 Dafny 的功能。有谁知道是否有一种方法可以在“reads”子句中使用量词,或者告诉 Dafny 读取包含对象的数组的每个条目中的字段?
感谢您的帮助。
最佳答案
您可以通过使用 set
作为 reads
子句来最轻松地做到这一点。
对于您的示例,vertexIsValid
上的这个附加 reads
子句对我有用:
reads set m | 0 <= m < vertices.Length :: vertices[m]
您可以将此 set
表达式视为“所有元素 vertices[m]
的集合,其中 m
在边界内”。
关于arrays - Dafny:将 "forall"量词与 "reads"或 "modifies"子句一起使用,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/48429725/