典型ArrayList插入操作中可变数组的Dafny框架验证问题

问题描述 #

以下是一个Dafny的ArrayList实现代码：

class ArrayListImpl<T(0)> {
    var xs: array<T>
    var n: nat

    predicate Valid() reads this
    { 0 <= n <= xs.Length }

    constructor(cap:nat) 
      requires cap > 0
      ensures Valid()
    {
      xs := new T[cap];
      n := 0;
    }

    function Size(): nat reads this
      requires Valid()
    { n }

    function Get(i:nat): T
        reads this, {xs}
        requires Valid()
        requires 0 <= i < Size() 
    { xs[i] }

  method Insert(i:nat, x:T)
      modifies this, {xs}

      requires 0 <= n <= xs.Length
      requires 0 <= i <= Size()
      requires !(n == xs.Length)

      ensures  0 <= n <= xs.Length
      ensures  Size() == old(Size()) + 1
      ensures  forall j :: 0 <= j < i           ==> Get(j) == old(Get(j))   
      ensures  forall j :: i < j <= old(Size()) ==> Get(j) == old(Get(j-1))
      ensures  Get(i) == x                                                   
    {
      var k := n;
      while k > i
        invariant 0 <= n <= xs.Length && n == old(n)
        invariant i <= k <= n < xs.Length    
        invariant forall j :: 0 <= j < i ==> xs[j] == old(xs[j])   
        invariant forall j :: k < j <= n ==> xs[j] == old(xs[j-1])  
        invariant forall j :: i <= j < k ==> xs[j] == old(xs[j])      
        invariant xs[i] == old(xs[i]) 
        decreases k - i
      {
        xs[k] := xs[k-1];  // update issue
        k := k - 1;
      }
      xs[k] := x;   // update issue
      n := n + 1;
    }
}

运行验证时，Insert方法中的数组赋值操作报错：

assignment might update an array element not in the enclosing context's modifies clause

用户尝试添加ghost变量oldSlice及后置条件ensures multiset(xs[..]) == multiset(old(xs[..]))，但问题未解决。使用Dafny版本为4.10。

问题原因 #

Dafny中，modifies子句里的{xs}表示数组对象的引用本身（即修改xs指向的数组实例），而非数组的元素。而Insert方法中是修改数组xs的元素值，并非替换整个数组，因此原modifies子句未覆盖元素修改的权限。

解决方案 #

将Insert方法的modifies子句修改为：

modifies this, xs[..]

xs[..]表示数组xs的所有元素，明确授权修改数组的全部元素。也可以更精确地指定元素范围（比如xs[0..xs.Length]），效果一致。

修改后的Insert方法头部如下：

method Insert(i:nat, x:T)
    modifies this, xs[..]

    requires 0 <= n <= xs.Length
    requires 0 <= i <= Size()
    requires !(n == xs.Length)

    ensures  0 <= n <= xs.Length
    ensures  Size() == old(Size()) + 1
    ensures  forall j :: 0 <= j < i           ==> Get(j) == old(Get(j))   
    ensures  forall j :: i < j <= old(Size()) ==> Get(j) == old(Get(j-1))
    ensures  Get(i) == x

修改后，验证器会认可数组元素的修改操作，代码可正常通过验证。

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