Dafny 4中无法证明对象序列修改的验证问题求助

你在Dafny中实现了closeCarPark方法，意图将停车场的所有车位设置为未占用状态，但在Main中调用该方法时无法通过验证。移除方法的modifies子句和修改属性的代码后验证通过，核心疑问是为何Dafny无法证明Spaces序列中的对象正在被修改。

相关代码 #

closeCarPark方法

method closeCarPark(Spaces: seq<ParkingSpace>) returns (newSpaces: seq<ParkingSpace>)
      modifies set space | space in Spaces
   {
      var i := 0;

      while i < |Spaces|
         invariant 0 <= i <= |Spaces|
      {

         Spaces[i].setOccupied(0);

         i := i + 1;
      }

      return Spaces;
   }

调用代码

carPark.Spaces := carPark.closeCarPark(carPark.Spaces);

ParkingSpace类实现

class ParkingSpace {    
    var SpaceID: int    
    var Occupied: int    
    var Reservation: string    
    var Location: string    
    var Car: Car?    
    ghost var repr: set<object>
    
    constructor(id: int, filled: int, reservation: string, location: string) 
        requires id != 0
        requires filled == 0 || filled == 1
        requires (location == "Regular" || location == "Subscription") && location != ""
        requires (reservation == "None" || |reservation| == 7) && reservation != "" 
        requires forall i :: 0 <= i < |reservation| ==> ('a' <= reservation[i] <= 'z' || 'A' <= reservation[i] <= 'Z' || '0' <= reservation[i] <= '9')    
    {
        SpaceID := id;
        Occupied := filled;
        Reservation := reservation;
        Location := location;
        Car := null;

        this.repr := this.repr + {this};    
    }
    
    method setOccupied(count: int) 
        modifies this
        ensures this.Occupied == count;
    {
        this.Occupied := count;
    }
}

核心原因 #

Dafny的验证器需要严格证明方法的modifies子句与实际修改操作完全匹配，这里无法通过验证的关键在于两点：

1. 循环不变式缺失关键约束
   你的循环仅声明了0 <= i <= |Spaces|的不变式，但没有明确断言Spaces参数在循环执行期间保持不变。Dafny的验证器不会默认假设方法参数（尤其是引用类型的序列）不会被修改，因此它无法确定循环中每次访问的Spaces[i]始终属于方法modifies子句中声明的set space | space in Spaces集合。

2. modifies子句的关联证明不足
   虽然setOccupied方法明确声明modifies this，但Dafny需要证明Spaces[i]确实是modifies子句中指定的对象之一。由于缺少Spaces参数不变的断言，验证器无法确认循环过程中Spaces序列未被篡改，也就无法保证Spaces[i]始终属于初始传入的车位对象集合。

解决办法 #

修改closeCarPark方法的循环不变式，添加Spaces == old(Spaces)来明确参数序列在循环中保持不变：

method closeCarPark(Spaces: seq<ParkingSpace>) returns (newSpaces: seq<ParkingSpace>)
      modifies set space | space in Spaces
   {
      var i := 0;

      while i < |Spaces|
         invariant 0 <= i <= |Spaces|
         invariant Spaces == old(Spaces)  // 新增不变式，确保序列本身未被修改
      {
         Spaces[i].setOccupied(0);
         i := i + 1;
      }

      return Spaces;
   }

这个不变式告诉Dafny：在循环的每一次迭代中，Spaces参数始终等于方法刚被调用时的初始值，因此每次访问的Spaces[i]必然属于modifies子句中声明的对象集合，验证器就能顺利证明修改操作的合法性。

内容的提问来源于stack exchange，提问作者Oliver haythornthwaite