Как избежать убавок и модифицировать нарушение?

Как я могу избежать ошибки уменьшения, если мой индекс не будет уменьшаться после каждой итерации? И почему я получаю предложение модификации для объекта и массива, в то время как я использую для них предложение модификации?

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 другому объекту из-за других проблем с нарушениями модификации. Но здесь кажется, что язык дафни ограничен, не так ли?


automated-tests solidity dafny
person Jaroxa    schedule 30.12.2017    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Вы пишете modifies this.m_owners, но когда вы собираетесь изменить this.m_owners, Дафни не знает, что this.m_owners по-прежнему относится к тому же объекту, что и в начале метода.

Попробуйте добавить эти инварианты в свои циклы while,

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

Для предложения уменьшения вам нужно будет доказать Дафни, что m_numOwners - frees на самом деле уменьшается, что мне не кажется верным - мне кажется, что может быть так, что оба внутренних условия цикла while будут ложными, в котором случае ни m_numOwners, ни frees не изменятся. Это может быть ошибка в вашем коде, или, может быть, вам нужно больше предварительных условий и инвариантов, я не уверен в ваших намерениях.

person tjhance    schedule 27.01.2020