dafny

Question

所以在我试图完成的 Dijkstra 算法的实现中，我有一个 class 顶点和 class 边。它看起来像这样：

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

  constructor Init()
  modifies this
  {
  this.wfs :=-1;
  this.pred := -1;
  } 
}

class Edge{
  var source : int;
  var dest: int;
  var weight : int;
}

和如下所示的图表 class：

class Graph{
  var vertices : set<Vertex>
  var edges : set<Edge>
  var d : array<int>
}

带有一堆关于算法运行中假定的图的谓词。我正在尝试编写一种方法，该方法将顶点作为输入，然后输出该顶点的源的当前最短路径，该路径存储在 d 中，其中 d 的索引是顶点的 "id" 。该方法如下所示：

method getVertexwfs(v: Vertex) returns (i: int)
  requires isValid() && hasVertex(v) && v != null
  requires hasVertex(v) ==> 0 <= v.id < d.Length && v in vertices
  ensures  exists s :: 0 <= s < d.Length && d[s] == i 
  {
   var x: int := 0;
    while (x < d.Length)
     invariant  hasVertex(v)
     invariant hasVertex(v) ==> 0 <= v.id < d.Length
     invariant v in vertices && 0 <= v.id < d.Length
        {
            if(v.id == x){ i := d[x]; }
            x := x + 1 ;
        }
   //return i;
  }

其中涉及的谓词是：

predicate isValid()
  reads this, this.edges, this.vertices
  {
  d != null && |vertices| > 0 && |edges| > 0 &&
  d.Length == |vertices| &&
  forall m | m in vertices :: (m != null && 0 <= m.id < d.Length ) &&
  forall m , n | m in vertices && n in vertices && m != n :: (m != null && n 
!= null && m.id != n.id) &&
  forall e | e in edges :: e != null && 0 <= e.source <= e.dest < d.Length &&
  forall e | e in edges :: !exists d | d in edges :: d != e &&  d.source == e.source && d.dest == e.dest
  }

和

predicate method hasVertex(v: Vertex)
  requires isValid()
  reads this, this.vertices, this.edges
  {
  vertices * {v} == {v}
  }

违反了 getVertexwfs() 方法的后置条件，尽管我坚持函数的前提条件是 v 存在于图中并且这意味着 v 的 ID 是 d 范围内的索引。

我是否遗漏了 Dafny 发现未分配 return 整数的情况？

为什么违反了前提条件？

感谢任何帮助。

Answer 1

在getVertexwfs中，我觉得我一定是错过了什么。为什么后置条件不能是 ensures d[v.id] == i？为什么 body 不能是 i := d[v.id];。循环似乎没有做任何有趣的事情；它只是不必要地从 0 搜索到 v.id。

此外，在hasVertex中，您可以只写v in vertices。相当于你拥有的。

最后，在 isValid 中，您需要将量词括起来，例如 (forall m | m in vertices :: m != null && 0 <= m.id < d.Length)。否则，这意味着 forall 继续到谓词的末尾。此外，在现代 Dafny 中，用作类型的类名自动暗示 non-nullness。如果您从未打算将 null 存储在数据结构中，则可以保留类型不变，只需删除 isValid 中所有谈论不是 null 的部分。

如果我进行这些更改，程序会进行验证。

dafny - 令人费解的后置条件违规

dafny - puzzling postcondition violation

formal-verification

graph-algorithm