Dafny 中使用 PriorityQueue 的 Dijkstras 算法

Question

所以我试图在 Dafny 中制作 Dijkstra 算法。我编写了一个自定义 Pair 类：

class Pair <U,V>{
  var first:U
  var second:V

  constructor (x:U, y:V) 
  ensures first == x
  ensures second == y
  {
    first := x;
    second := y;
  }
  function getFirst():U
  reads this
  {
    first
  }
  function getSecond():V
  reads this
  {  
    second
  }
}

以及后来用于主要算法的自定义 PriorityQueue 和 Graph 类：

class PriorityQueue {
  var heap: array<Pair<int, int>>
  var size: int
  var capacity: int

  constructor (private_capacity: int)
  requires private_capacity > 0 
  ensures heap.Length == capacity
  ensures size <= heap.Length
  ensures size < capacity
  ensures size == 0
  {
    capacity := private_capacity;
    size := 0;
    var default := new Pair<int, int>(0, 0);
    heap := new Pair<int, int>[private_capacity](_ => default);
  }

  method parent(i: int) returns (p: int)
  requires 0 <= i < size
  requires i < heap.Length
  ensures p < heap.Length
  ensures i > 0 ==> 0 <= p < size
  ensures i == 0 ==> p == -1
  {
    if i > 0 {
      p := (i - 1) / 2;
    } else {
      p := -1;
    }
  }

  method leftChild(i: int) returns (l: int)
  requires 0 <= i < size
  ensures l == 2 * i + 1
  {
    l := 2 * i + 1;
  }

  method rightChild(i: int) returns (r: int)
  requires 0 <= i < size
  ensures r == 2 * i + 2
  {
    r := 2 * i + 2;
  }

  method swap(i: int, j: int)
  requires 0 <= i < size && 0 <= j < size
  requires i < heap.Length && j < heap.Length
  modifies heap
  ensures heap[i] == old(heap[j]) && heap[j] == old(heap[i])
  {
    var temp := heap[i];
    heap[i] := heap[j];
    heap[j] := temp;
  }

  method heapifyUp(i: int)
  requires 0 <= i < size
  requires size <= heap.Length
  modifies heap
  decreases i
  {
    var current_parent := parent(i);

    if current_parent >= 0 && current_parent < size
      && 0 <= current_parent < size 
      && heap[i].second < heap[current_parent].second 
    {
      swap(i, current_parent);
      if (current_parent < i) {
        heapifyUp(current_parent); 
      }
    }
  }

  method heapifyDown(i: int)
  requires 0 <= i < size
  modifies heap
  decreases size - i
  {
    var smallest := i;
    var left_child := leftChild(i);
    var right_child := rightChild(i);
    if left_child < size && left_child < heap.Length && heap[left_child].second < heap[smallest].second {
      smallest := leftChild(i);
    }
    if right_child < size && right_child < heap.Length && heap[right_child].second < heap[smallest].second {
      smallest := rightChild(i);
    }
    if smallest != i {
      swap(i, smallest);
      heapifyDown(smallest);
    }
  }

  method insert(item: int, priority: int)
  requires heap.Length == capacity
  requires 0 <= size < capacity
  modifies this, heap
  {
    heap[size] := new Pair<int, int>(item, priority);
    size := size + 1;
    heapifyUp(size - 1);
  }

  method extractMin() returns (item: int)
  requires size > 0
  requires heap.Length > 0
  requires size - 1 < heap.Length
  modifies this, heap
  ensures size == old(size) - 1
  {
    item := heap[0].first;
    heap[0] := heap[size - 1];
    size := size - 1;
    if size > 0 {
      heapifyDown(0);
    }
  }

  // Peek the element with the smallest priority without removing it
  method peek() returns (item: int)
  requires size > 0
  requires heap.Length > 0
  ensures item == heap[0].first
  {
    item := heap[0].first;
  }

  // Check if the priority queue is empty
  method isEmpty() returns (empty: bool)
  ensures empty == (size == 0)
  {
    empty := (size == 0);
  }
}

class Graph {
  var adj: map<int, seq<Pair<int, int>>>
  var numNodes: int

  constructor (nodes: int, edges: map<int, seq<Pair<int, int>>>)
  ensures adj == edges
  ensures numNodes == nodes
  {
    adj := edges;
    numNodes := nodes;
  }
}

在我看来这些看起来不错，但是当我尝试实现 Dijkstras 方法时，该方法在类之外：

method Dijkstra(graph: Graph, start: int) returns (distances: map<int, int>)
requires 0 <= start < graph.numNodes
requires forall n :: n in graph.adj ==> 0 <= n < graph.numNodes
{
  var pq := new PriorityQueue(graph.numNodes);
  pq.insert(start, 0);
  
  var inf := 1000000000; // Representation of infinity

  var initMap := map n | n in graph.adj :: inf;
  distances := initMap[start := 0];


  while true
  invariant forall n :: n in graph.adj ==> distances[n] >= 0
  invariant distances[start] == 0
  {
    var empty := pq.isEmpty();
    if empty {
      break;
    }

    var u := pq.extractMin();

    if u in graph.adj {
      var edges := graph.adj[u];
      for i := 0 to |edges| - 1 {
        var edge := edges[i];
        var v := edge.first;
        var weight := edge.second;

        if distances[u] + weight < distances[v] {
          distances := distances[v := distances[u] + weight];
          pq.insert(v, distances[v]);
        }
      }
    }
  }

}

我遇到了多个错误，主要是

call might violate context's modifies clause

对于

pq.insert(start, 0)

和

var u := pq.extractMin()

我的问题是：我的类是否针对 dijkstras 算法进行了良好编程？我在 Dijkstra 方法中缺少什么，而 verifire 不批准我的算法？

我将错误范围缩小到可能是优先队列的

insert

函数。如果我删除修改子句，则验证不会在 dijkstra 的算法方法中发现任何错误，但它会对我大喊大叫，因为我正在修改

heap

和

size

数组和变量。

Answer 1

您在构造函数中缺少

ensures fresh(heap)

子句。