Сбит с толку сообщениями постусловия Dafny

Очень простой код умножения:

method Product1 (m: nat, n: nat) returns (res:nat) 
ensures res == m * n;      
{  
    var m1: nat := 0; 
    var n1: nat := 0; 
    res := 0; 
    while (m1 < m)    
    { 
        n1 := 0; 
        while (n1 < n)  
        { 
            res := res + 1;
            n1 := n1 + 1; 
        } 
        m1 := m1 + 1; 
    } 
}

Когда я проверяю это с помощью dafny, он говорит:

    Description                                        Line Column
1   A postcondition might not hold on this return path. 8   4
2   This is the postcondition that might not hold.      2   16

Я понимаю, что при некоторых условиях там написано res != m*n, но я не могу понять.


verification dafny
person Richard Yang    schedule 14.09.2016    source источник
comment
Кроме того, пожалуйста, не просите людей считать номера строк. Добавьте комментарии к оскорбительным строкам.   -  person candied_orange    schedule 14.09.2016
comment
Сообщение постусловия не означает, что res != m*n, скорее это означает, что Дафни не может доказать, что res == m*n во всех случаях. Вот почему он говорит, что может не держаться.   -  person lexicalscope    schedule 20.09.2016

Ответы (2)


arrow_upward
3
arrow_downward

Обновлено!

Пробовал dafny на онлайн-сайте, похоже, это ошибка?

method Test(m: nat) returns (r: nat) 
{
  var m1: nat := 0;
  while (m1 < m) {
    m1 := m1 + 1;
  }
  assert m == m1; // fail assert
}

еще попробуй:

method Test(m: nat) returns (r: nat) 
{
  var m1: nat := 0;
  while (m1 < m) {
    assert m1 < m;
    m1 := m1 + 1;
  }
  assert !(m1 < m);   // pass
  assert m1 == m || m1 > m;  // pass
  assert m1 == m;  // fail
}

После некоторого глубокого понимания я понял, что для ответа на этот вопрос следует использовать Loop Invariants вместо dafny.

Мой модифицированный код:

method Product1 (m: nat, n: nat) returns (res:nat) 
ensures res == m * n;      
{  
    var m1: nat := 0; 
    var n1: nat := 0; 
    res := 0; 
    while (m1 < m)
    invariant 0 <= m1 <= m
    invariant res == m1 * n
    { 
        var temp: nat := res; 
        n1 := 0; 
        while (n1 < n)
        invariant 0 <= n1 <= n
        invariant res == temp+n1   
        { 
            res := res + 1;
            n1 := n1 + 1; 
        } 
        m1 := m1 + 1; 
    }
    assert m1 == m;  // success
}

Затем удалите переменную tmp:

method Product1 (m: nat, n: nat) returns (res:nat) 
ensures res == m * n;      
{  
    var m1: nat := 0; 
    var n1: nat := 0; 
    res := 0; 
    while (m1 < m)
    invariant 0 <= m1 <= m
    invariant res == m1 * n
    {
        n1 := 0; 
        while (n1 < n)
        invariant 0 <= n1 <= n
        invariant res == n1 + m1*n  
        { 
            res := res + 1;
            n1 := n1 + 1; 
        } 
        m1 := m1 + 1; 
    }
    assert m1 == m;  // success
}
person Gohan    schedule 14.09.2016

arrow_upward
0
arrow_downward

Ваши циклы не имеют инвариантов циклов. Как минимум, вам понадобятся инварианты для обоих циклов. Иначе Дафни не сможет понять, что осталось после петель...

person redjamjar    schedule 14.09.2016