2

如果每次迭代后我的索引都不会减少，我如何避免减少错误？为什么我在一个对象和一个数组上得到一个修改子句，而我对它们使用修改子句？

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

  constructor(){
  new;
  }
}

class multiowned{

  var m_numOwners : int;
  var m_owners : array<int>;
  var m_ownerIndex : ownerIndexs;

method reorganizeOwners() returns (boo : bool)
  requires m_owners != null && m_ownerIndex != null
  requires  m_owners.Length >= 2
  requires 0 <= m_numOwners < m_owners.Length


  modifies this
  modifies this.m_owners 
  modifies this.m_ownerIndex;
 {
    var frees : int := 1;
    while (frees < m_numOwners)
    decreases m_numOwners - frees      //error 1
    invariant m_owners != null && m_numOwners < m_owners.Length
    invariant m_ownerIndex != null


    {
        while (frees < m_numOwners && m_owners[frees] != 0)
        decreases m_numOwners - frees
        invariant frees <= m_numOwners
        invariant m_owners != null && m_numOwners < m_owners.Length
        invariant m_ownerIndex != null
        {
          frees := frees +1;
        }

       while (m_numOwners > 1 && m_owners[m_numOwners] == 0)
       invariant m_owners != null && m_numOwners < m_owners.Length
       invariant m_ownerIndex != null
        {
          m_numOwners := m_numOwners-1;
       }
 if (frees < m_numOwners && m_owners[m_numOwners] != 0 && m_owners[frees] == 0)
        {
            m_owners[frees] := m_owners[m_numOwners]; //error 2
            m_ownerIndex.oi := m_ownerIndex.oi[m_owners[frees] := frees]; //error 3
            m_owners[m_numOwners] := 0;
        }
    }
    boo := true;
  }

}

我也在 Dafny 中上传了此代码，您可以在其中再次编译它：https ://rise4fun.com/Dafny/bYDH 。如您所见，由于其他修改违规问题，我修改了数组 m_owner 并将 ownerIndex 外包给另一个对象。但是在这里，dafnys 的语言似乎是有限的，不是吗？

4

1 回答 1

1

你写modifies this.m_owners了但是当你去 modify 时this.m_owners，Dafny 不知道它this.m_owners仍然指的是同一个对象，就像它在方法开始时所做的那样。

尝试将这些不变量添加到您的 while 循环中，

    invariant this.m_owners == old(this.m_owners)
    invariant this.m_ownerIndex == old(this.m_ownerIndex)

对于减少子句，您需要向 Dafny 证明m_numOwners - frees实际上减少了，这对我来说似乎并不正确 - 在我看来，可能是两个内部 while 循环条件都为假的情况，在这种情况下不会m_numOwners也frees不会改变。这可能是您的代码中的错误，或者您可能需要更多的先决条件和不变量，我不确定您的意图。

于 2020-01-27T16:36:18.310 回答