1

如何在方法中覆盖标记为已修改的数组？或者在 Dafny 中有没有办法将数组的长度增加一倍？

class ownerIndexs{
 var oi : map<int, int>;

 constructor(){
 new;
 }
}

class Pendingstate{
 var yetNeeded : int;
 var ownersDone : bv256;
 var index : int;
} 

class mo{
 var m_pendingIndex : array<int>;
 var m_ownerIndex : ownerIndexs;
 var m_pending : map<int, Pendingstate>;
 var m_required : int;

 method confirmAndCheck(operation : int, msgsender : int) returns
  (boo : bool, ownerIndex :int,pending : Pendingstate)

  requires m_pendingIndex != null
  modifies this.m_pendingIndex

  ensures m_pendingIndex != null && pending != null 
          ==> 0 < pending.index < m_pendingIndex.Length 
          && m_pendingIndex[pending.index] == operation
    {
    pending := new Pendingstate;
    pending.index := m_pendingIndex.Length;
    this.m_pendingIndex := extendArrayByOne(this.m_pendingIndex); //Problem with modify clause
    m_pendingIndex[pending.index] :=  operation;

    }

method extendArrayByOne(oldarray:array<int>) returns (newarray:array<int>)
 requires oldarray!=null
 ensures newarray != null
 ensures fresh(newarray)
 ensures newarray.Length == oldarray.Length+1
 ensures forall k::0 <= k <oldarray.Length ==> oldarray[k] == newarray[k]
 modifies oldarray
 {
   newarray := new int[oldarray.Length+1];
   var i:=0;
   while (i < oldarray.Length)
    invariant newarray.Length == oldarray.Length+1
    invariant i<=oldarray.Length
    invariant forall k::0 <= k < i ==> oldarray[k] == newarray[k]
   {
     newarray[i] := oldarray[i];
     i := i + 1;
   }
 }

}

正如您在这段代码中看到的那样。我试图在方法extendArrayByOne 中将数组的长度增加一。之后，我在方法 confirmAndCheck 中添加从 extendArrayByOne 返回的新数组末尾的元素操作。这是官方编译器的链接，可以编译此代码： https ://rise4fun.com/Dafny/WtjA

这是我之前关于extendArrayByOne的问题的链接：

修改已更改对象的子句错误

4

0 回答 0