Dafny: Using "forall" quantifiers with the "reads" or "modifies" clauses

Question

So I am trying to implement Dijkstra's single source shortest paths algorithm in Dafny based directly on the description of the algorithm in the CLRS algorithms book as part of an undergraduate project. As part of the implementation, I have defined a "Vertex" object with two fields representing the current length of shortest path from source and the predecessor vertex:

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

As well as a "Graph" object that contains an array of "Vertex"-es:

    class Graph{
    var vertices: array<Vertex>;
    ....

I am trying to state some properties of the fields in each "Vertex" of the vertices array using a predicate in the "Graph" object:

    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
     }

To my understanding, the "reads" and "modifies" clauses in Dafny only work on one layer and I'd have to specify to Dafny that I would be reading each entry in the vertices array ( reads this.vertices[x] ) . I tried using a "forall" clause to do it:

   forall m :: 0 <= m < vertices.Length ==> reads this.vertices[m]

but this doesn't seem to be a feature in Dafny. Does anyone know if there is a way to use quantifiers with the "reads" clause or otherwise tell Dafny to read the fields in each entry of an array containing objects?

Thanks for the help.

Answer 1

You can do that most easily by using a set as a reads clause.

For your example, this additional reads clause on vertexIsValid worked for me:

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

You can think of this set expression as saying "the set of all elements vertices[m] where m is in bounds".