Norbert Horváth's questions

Estou tentando fazer o algoritmo de Dijkstra em Dafny. Programei uma classe Pair personalizada:

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

e mais tarde uma classe PriorityQueue e Graph personalizada para o algoritmo principal:

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

Na minha opinião, elas parecem boas, mas quando tentei implementar o método Dijkstras, que está fora das classes:

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

}

Recebo vários erros, principalmente

chamada pode violar a cláusula de modificação do contexto

para ambos pq.insert(start, 0)evar u := pq.extractMin()

O que estou esquecendo no método de Dijkstra, para o qual o verificador não aprova meu algoritmo?

Reduzi o erro para provavelmente ser a insertfunção da fila de prioridades. Se eu remover as cláusulas modifies, o verifys não encontra nenhum erro no método do algoritmo de Dijkstra, mas ele vai gritar comigo porque estou modificando o array heapand sizee a variável.