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

问题描述 投票:2回答:1

所以我在Dijkstra算法的实现中有一个类Vertex和class Edge,我试图完成。它看起来像这样:

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;
}

和一个如下所示的Graph类:

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

在运行算法时假设有一堆关于图的谓词。我正在尝试编写一个方法,将Vertex作为输入,然后从该顶点的源输出当前最短路径,该路径存储在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}
  }

尽管我坚持在图中存在v的函数的前提条件,但是这意味着v的ID是d的边界中的索引,否则违反了getVertexwfs()方法的后置条件。

我错过了Dafny发现未分配返回整数的情况吗?

为什么违反前提条件?

任何帮助表示赞赏。

graph-algorithm formal-verification dafny
1个回答
2
投票

getVertexwfs,我觉得我必须遗漏一些东西。为什么后置条件不能成为ensures d[v.id] == i?为什么身体不能成为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中,用作类型的类名自动暗示非归零。如果你从未计划在数据结构中存储null,你可以保留类型与它们相同,只删除isValid所有谈论不是null的部分。

如果我进行了这些更改,程序将进行验证。

© www.soinside.com 2019 - 2024. All rights reserved.