Почему это утверждение Дафни, связанное с массивами, терпит неудачу?

Question

Я работаю над проверенной реализацией gaussian исключения, и у меня возникают проблемы с проверкой этого супер простого метода, который добавляет содержимое массива b в содержимое массива a. Вот код.

method addAssign(a: array<real>, b: array<real>) 
    requires a != null && b != null && a.Length == b.Length; 
    modifies a 
    ensures forall k:: 0 <= k < a.Length ==> a[k] == old(a[k]) + b[k]; 
{ 
    var i := 0; 
    assert a == old(a); 
    while(i < a.Length) 
     invariant 0 <= i <= a.Length 
     invariant forall k:: i <= k < a.Length ==> a[k] == old(a[k]) 
     invariant forall k:: 0 <= k < i ==> a[k] == old(a[k]) + b[k]; 
    { 
     assert a[i] == old(a[i]); // dafny verifies this 
     a[i] := a[i] + b[i]; 
     assert a[i] == old(a[i]) + b[i]; // dafny says this is an assertion violation 
     i := i + 1; 
    } 
} 

Answer 1

(Я удалил свой первый ответ, так как он не работал).

Похоже, проблема заключается в том, что Дафни обнаруживает потенциальные проблемы с псевдонимом. В качестве эксперимента, я первый модифицированного код, чтобы получить еще более простую функцию, которая делает проверки:

method addOne(a: array<real>) 
    requires a != null; 
    modifies a; 
    ensures forall k:: 0 <= k < a.Length ==> a[k] == old(a[k]) + 1.0; 
{ 
    var i := 0; 
    assert a == old(a); 
    while(i < a.Length) 
     invariant 0 <= i <= a.Length 
     invariant forall k:: i <= k < a.Length ==> a[k] == old(a[k]) 
     invariant forall k:: 0 <= k < i ==> a[k] == old(a[k]) + 1.0; 
    { 
     assert a[i] == old(a[i]); // dafny verifies this 
     a[i] := a[i] + 1.0; 
     assert a[i] == old(a[i]) + 1.0; // dafny *doesn't* say this is an assertion violation 
     i := i + 1; 
    } 
} 

Единственным отличие состоит в том, что я использую буквальный реальный (1,0), а не реальный взято из b. Почему должно , что изменить ситуацию?

Ну предположим, что вы вызываете ваш метод с вызовом, который выглядит как

addAssign(a,a) 

то в теле функции b и a оба относятся к одной и той же матрицы. Предположим, например, что a[0] составляет 1,0. Затем в первом проходе через цикл вы выполняете a[0] := a[0] + b[0].

Это устанавливает a[0] в 2.0. Но - это также комплектов b[0] до 2.0.

Но в этой ситуации assert a[0] == old(a[0]) + b[0] эквивалентно

assert 2.0 == 1.0 + 2.0 - который должен неудачу.

Кстати - следующий делает проверить:

method addAssign(a: array<real>, b: array<real>) 
    requires a != null && b != null && a.Length == b.Length; 
    modifies a; 
    ensures forall k:: 0 <= k < a.Length ==> a[k] == old(a[k]) + old(b[k]); 
{ 
    var i := 0; 
    assert a == old(a); 
    while(i < a.Length) 
     invariant 0 <= i <= a.Length 
     invariant forall k:: i <= k < a.Length ==> a[k] == old(a[k]) 
     invariant forall k:: 0 <= k < i ==> a[k] == old(a[k]) + old(b[k]); 
    { 
     assert a[i] == old(a[i]); // dafny verifies this 
     a[i] := a[i] + b[i]; 
     assert a[i] == old(a[i]) + old(b[i]); // and also this! 
     i := i + 1; 
    } 
}