CODEWITHSUNDEEP
graph-algorithmformal-verificationdafny
NTDY
NTDY

Reputation: 67

dafny - puzzling postcondition violation

so I have a class Vertex and class Edge in an implementation of Dijkstra's algorithm that I am trying to complete. it looks like this:

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

and a Graph class that looks like this: 

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

with a bunch of predicates about the graph that are assumed in the running of the algorithm. I am trying to write a method that takes a Vertex as an input and then outputs the current shortest path from source for that vertex, which is stored in d, where the index of d is the "id" of the vertex. The method looks like this:

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

Where the involved predicates are:

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
  }

and

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

The postcondition for the getVertexwfs() method is violated, despite my insistence in the preconditions for the function that v exists in the Graph and that this implies that the ID for v is an index in the bounds of d.

Am I missing a case where Dafny finds that the return integer is not assigned?

Why is the precondition violated?

Any help is appreciated.

Upvotes: 2

Views: 237

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

In getVertexwfs, I feel like I must be missing something. Why can't the postcondition be ensures d[v.id] == i? And why can't the body be i := d[v.id];. The loop doesn't seem to do anything interesting; it just unnecessarily searches from 0 to v.id.

Also, in hasVertex, you can just write v in vertices. It's equivalent to what you have.

Finally, in isValid, you need to put parentheses around your quantifiers, like this (forall m | m in vertices :: m != null && 0 <= m.id < d.Length). Otherwise, it means that the forall continues to the end of the predicate. Also, in modern Dafny, the classnames used as types imply non-nullness automatically. If you never plan to store null in the data structure, you can leave the types the same as they are and just delete all the parts of isValid that talk about not being null.

If I make these changes, the program verifies.

Upvotes: 2

Related Questions