Как доказать инварианты цикла во вставке?
У меня возникли проблемы с написанием правильных инвариантов цикла для моего алгоритма сортировки вставками, перечисленного ниже. Я пытаюсь доказать, что все элементы в массиве до текущего индекса уже отсортированы, как и должна делать сортировка вставками, но Дафни не распознает мои инварианты должным образом.
method Sort(a : array<int>)
modifies a
ensures forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
{
var i := 0;
while (i < a.Length)
invariant 0 <= i <= a.Length
invariant forall x,y :: 0 <= x < y < i ==> a[x] <= a[y]
{
var j := i - 1;
while (j >= 0 && a[j] > a[j + 1])
invariant forall k,l :: 0 <= k < l <i ==> a[k] <= a[l]
{
a[j], a[j + 1] := a[j + 1], a[j];
j := j - 1;
}
i := i + 1;
}
}
Я пытался утверждать, что a[j] <= a[j+1] вне цикла, но Дафни, кажется, не думает, что это правда, несмотря на то, что он нормально работает внутри цикла после замены. Когда я пытаюсь использовать числа вне цикла, такие как a[0] <= a[1], это тоже не проверяется, и я не уверен, почему.
Ответы 1
Ваш инвариант внутреннего цикла не кажется мне правильным. Во время итерации он не держится. Например сделать следующий снимок во время сортировки вставкой.
i = 3
j = 1
init arr = [5, 4, 3, 2, 1]
arr at start of inner loop = [3, 4, 5, 2, 1]
curr arr = [3, 4, 2, 5, 1]
Вам нужны определенные бухгалтерские факты, чтобы их можно было проверить.
Допустим, вы вставляете элемент в i в [0..(i-1)].
Рассмотрим расширенный фрагмент [0..i], этот фрагмент отсортирован, если
мы сравниваем с элементом, который в настоящее время вставляем. Первый
инвариант фиксирует это. Второй инвариант, который необходимо
поддерживаться, если в настоящее время вставляемое число равно
по индексу j сортируется срез [j..i].
method sort(a: array<int>)
modifies a
ensures forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
{
var i := 0;
while i < a.Length
invariant 0 <= i <= a.Length
invariant forall m, n :: 0 <= m < n < i ==> a[m] <= a[n]
{
var j := i - 1;
while j >= 0 && a[j] > a[j+1]
invariant -1 <= j <= i - 1
invariant forall m, n :: 0 <= m < n <= i && ((m != j + 1) && (n != j + 1)) ==> a[m] <= a[n]
invariant forall m :: j < m <= i ==> a[j+1] <= a[m]
{
a[j], a[j+1] := a[j+1], a[j];
j := j - 1;
}
i := i + 1;
}
}