在Dafny中实现带PriorityQueue的Dijkstra算法时的modifies子句错误排查

核心问题：权限声明不匹配 #

Dafny的验证器严格要求方法明确声明自己会修改哪些对象/状态，你的错误根源是Dijkstra方法未声明允许修改传入的PriorityQueue实例，同时PriorityQueue的方法必须保留正确的modifies子句来声明修改自身成员。

具体解决步骤 #

1. 为Dijkstra方法添加modifies声明
   在Dijkstra方法的签名中，明确声明它会修改传入的PriorityQueue对象（如果pq是局部变量，也要在方法内或签名中声明）。示例：

   method Dijkstra(g: Graph, start: int, pq: PriorityQueue) returns (dist: array<int>)
     modifies pq; // 声明该方法允许修改pq实例的内部状态
   {
     pq.insert(start, 0);
     var u := pq.extractMin();
     // 后续算法逻辑
   }
   

   如果pq是Dijkstra方法内创建的局部变量，也需要在方法签名或内部声明修改权限：

   method Dijkstra(g: Graph, start: int) returns (dist: array<int>)
   {
     var pq := new PriorityQueue();
     modifies pq;
     pq.insert(start, 0);
     // ...
   }
   

2. 保留PriorityQueue方法的modifies子句
   PriorityQueue的insert和extractMin方法必须声明修改自身（this），因为它们会操作类的成员变量（heap数组、size）。绝对不能移除这些子句，否则验证器会认为你在未经授权的情况下修改类成员。示例：

   class PriorityQueue {
     var heap: array<Pair>;
     var size: int;
   
     method insert(node: int, weight: int)
       modifies this; // 明确声明修改当前对象的成员
     {
       // insert实现逻辑
     }
   
     method extractMin() returns (node: int)
       modifies this; // 同样声明修改当前对象
     {
       // extractMin实现逻辑
     }
   }
   

3. 补充类不变式增强验证能力
   为PriorityQueue添加类不变式，帮助Dafny验证器理解队列的合法状态（比如size的范围、堆结构的正确性），这能减少因状态合法性存疑导致的额外报错。示例：

   class PriorityQueue {
     var heap: array<Pair>;
     var size: int;
   
     // 基本状态不变式
     invariant 0 <= size <= heap.Length;
     // 最小堆结构不变式（根据你的Pair类定义调整）
     invariant forall i: int :: 1 <= i < size ==> heap[(i-1)/2].Weight <= heap[i].Weight;
   
     // 方法实现...
   }
   

关键逻辑说明 #

Dafny的modifies子句是验证器的“权限清单”：

• 当你调用一个带有modifies子句的方法时，调用方必须已经声明自己有权修改该方法要修改的对象。
• 类方法修改自身成员时，必须用modifies this声明，告诉验证器该方法会改变当前对象的状态。

内容的提问来源于stack exchange，提问作者Norbert Horváth