Дафни проверяет сортировку вставками, используя своп

Я работаю над тем, как использовать dafny для проверки сортировки вставками с помощью «перестановки» соседних элементов, но я не могу найти разумный инвариант для цикла while, может ли кто-нибудь помочь мне это исправить? Вот ссылка: http://rise4fun.com/Dafny/wmYME


swap loop-invariant insertion-sort dafny
person Lilac Liu    schedule 19.05.2017    source источник
comment
инвариант задачи находится в строке 19   -  person Lilac Liu    schedule 19.05.2017

Ответы (1)


arrow_upward
0
arrow_downward

Здесь есть несколько проблем.

Во-первых, ваш внутренний цикл неверен, потому что переменная temp никогда не обновляется. Я рекомендую удалить temp и вместо этого использовать условие цикла down >= 0 && a[down+1] < a[down].

Во-вторых, у вас есть несколько проблем с неправильно сформированным инвариантом внутреннего цикла (индекс вне допустимого диапазона, нарушение предварительного условия sorted). Однако вместо того, чтобы исправлять их, я рекомендую выбросить оба инварианта внутреннего цикла и повторить попытку.

Мой предпочтительный инвариант для внутреннего цикла сортировки вставками: «a[0..up+1] отсортировано, за исключением, возможно, down + 1». Вы можете указать это как

invariant forall j,k | 0 <= j < k < up+1 && k != down+1 :: a[j]<=a[k]

Полученный файл проверяется.

person James Wilcox    schedule 30.07.2017