如何避免减量和修改违规？

Question

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

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的语言是有限的，不是吗？

Answer 1

你写了modifies this.m_owners但是当你去修改this.m_owners的时候，Dafny并不知道this.m_owners仍然指的是和方法开始时一样的对象.

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

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

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

如何避免减量和修改违规？

How to avoid decreases and modify violation?

automated-tests

dafny

solidity