Моя задача — инициализировать матрицу 8x8 и убедиться, что все элементы внутри матрицы равны нулю. Я также должен использовать циклы while и инварианты циклов для реализации. Моя реализация выглядит так:
method initMatrix(a: array2<int>)
modifies a
// require an 8 x 8 matrix
requires a.Length0 == 8 && a.Length1 == 8
// Ensures that all rows in the matrix are zeroes
ensures forall row, col :: 0 <= row < a.Length0 && 0 <= col < a.Length1 ==> a[row, col] == 0
{
var row : nat := 0;
while(row < a.Length0)
invariant 0 <= row <= a.Length0
invariant forall i,j :: 0 <= i < row && 0 <= j < a.Length1 ==> a[i,j] == 0
{
var col : nat := 0;
while(col < a.Length1)
invariant 0 <= row <= a.Length0
invariant 0 <= col <= a.Length1
invariant forall i,j :: i == row && 0 <= j < col ==> a[i,j] == 0
{
a[row, col] := 0;
col := col + 1;
}
row := row + 1;
}
}
Логически я думаю, что все мои квантификаторы верны. Однако Дафни считает, что мой цикл инвариантен во внешнем цикле while.
invariant forall i,j :: 0 <= i < row && 0 <= j < a.Length1 ==> a[i,j] == 0
не поддерживается циклом.
Сначала я заподозрил, что проблема существует в моей реализации. Поэтому я сначала запустил метод без каких-либо предварительных и последующих условий и напечатал все элементы массива; на выходе была матрица, полная нулей.
Чтобы быть вдвойне уверенным, что он заменяет все элементы, а не просто использует нули с момента создания экземпляра матрицы, я инициализировал все элементы в матрице единицами и распечатал все значения внутри нее. Результат был тот же - все элементы в матрице были 1s.
Из этого эксперимента я могу сделать вывод, что проблема не в моей реализации, а в том, как я определял свои спецификации.
Я прошел свой алгоритм вручную и обнаружил, что он логически должен работать, однако я думаю, что мое понимание того, как квантификаторы работают в инвариантах цикла в Dafny, может быть искажено.
Что именно происходит, когда условие 0 <= i < row && 0 <= j < a.Length1 ложно? На первой итерации переменная row равна 0, что не удовлетворяет условию 0 <= i < row. Проходит ли он первую строку и проверяет, все ли элементы в этой строке равны нулю, или пропускает ее?
Что происходит, когда он достигает оператора row := row + 1; на начальной итерации? Использует ли инвариант цикла invariant forall i,j :: 0 <= i < row && 0 <= j < a.Length1 ==> a[i,j] == 0 значение row при входе (которое равно нулю) или использует увеличенное значение row (1)?
