Как найти петлю инварианта и доказать правильность?

Question

int i, temp; 
a is an array of integers [1...100] 

i = 1; 

while i < 100 
    if a[i] > a[i+1] 
        temp = a[i]
        a[i] = a[i+1]
        a[i+1] = temp 
    i = i+1

У меня проблемы с пониманием того, как найти инварианты цикла и написать для них формальное утверждение. Таким образом, инвариант цикла - это просто условие, которое выполняется непосредственно до и после каждой итерации цикла. Похоже, что код выполняет обмен: если следующий элемент больше в массиве, чем текущий, поменяйте местами. Я имею в виду из определения инварианта цикла, это действительно звучит так, как будто я < 100, потому что это должно быть верно для цикла, но я не совсем понимаю. Буду очень признателен за некоторые разъяснения.

Answer 1

Исходя из вашего определения, я вижу два условия инварианта цикла:

1. i < 100
2. a[i] = greater than a[j] for all j < i, where i is the loop variable.

На самом деле это одна итерация внешнего цикла пузырьковой сортировки. В конце этого цикла самое высокое значение в массиве всплывает наверх (a[100]) .

Answer 2

Грубо говоря, вы правы. Инвариант цикла - это "просто условие, которое выполняется непосредственно до и после каждой итерации цикла". Однако согласно этому определению существует буквально бесконечное число инвариантов цикла для рассматриваемого кода, и большинство из них не представляют особого интереса. Например, i < 101, i < 102, i < 103, ... являются инвариантами цикла для данного кода.

Однако обычно мы не заинтересованы в простом нахождении инварианта цикла только ради нахождения инварианта цикла. Вместо этого мы заинтересованы в том, чтобы доказать правильность программы, и если мы хотим доказать правильность программы, то хорошо выбранный инвариант цикла оказывается очень полезным.

Например, рассматриваемый код является внутренним циклом алгоритма пузырьковой сортировки, и его целью является сделать массив "более отсортированным". Следовательно, чтобы доказать полную корректность этого кода, мы должны доказать три вещи:

(1) Когда выполнение достигает конца кода, массив представляет собой перестановку массива в начале кода. (2) Когда выполнение достигает конца кода, число инверсий в массиве либо равно нулю, либо меньше числа инверсий в массиве в начале кода (это условие помогает нам доказать, что внешнее цикл алгоритма сортировки пузырьков прекращается). (3) Код заканчивается.

Чтобы доказать (1), нам нужно рассмотреть три пути выполнения (и инвариант цикла будет играть критическую роль при рассмотрении PATH 2).

(ПУТЬ 1) Рассмотрим, что происходит, когда выполнение начинается в начале кода и достигает вершины цикла в первый раз. Поскольку с этим путем выполнения ничего не сделано для массива, массив является перестановкой массива в начале кода.

(ПУТЬ 2) Теперь рассмотрим, что происходит, когда выполнение начинается в верхней части цикла, проходит вокруг цикла и возвращается в начало цикла. Если a[i] <= a[i+1], то перестановка не происходит, и, таким образом, массив все еще является перестановкой массива в начале кода (поскольку с ним ничего не сделано). Альтернативно, если a[i] > a[i+1], то обмен происходит. Тем не менее, массив по-прежнему является перестановкой массива в начале кода (поскольку своп является типом перестановки). Таким образом, всякий раз, когда выполнение достигает вершины цикла, массив является перестановкой массива в начале кода. Обратите внимание, что утверждение "массив - это перестановка массива в начале кода" - это правильно выбранный инвариант цикла, который нам нужен, чтобы помочь нам доказать, что код верен.

(ПУТЬ 3) Наконец, рассмотрим, что происходит, когда выполнение начинается в верхней части цикла, но не входит в цикл, а вместо этого идет в конец кода. Поскольку с этим путем выполнения ничего не сделано для массива, массив является перестановкой массива в начале кода.

Эти три пути охватывают все возможные пути выполнения от начала кода до конца кода, и, следовательно, мы доказали (1), что массив в конце кода является перестановкой массива в начале кода.

Answer 3

Инвариант цикла - это некоторый предикат (условие), который выполняется для каждой итерации цикла, что обязательно верно непосредственно перед и сразу после каждой итерации цикла.

Конечно, может быть бесконечно много инвариантов цикла, но тот факт, что свойство инварианта цикла используется для доказательства правильности алгоритма, ограничивает нас в рассмотрении только так называемых "интересных инвариантов цикла".

Ваша программа, целью которой является сортировка заданного массива, является простой пузырьковой сортировкой.

Goal Statement: The array a is sorted at the end of while loop
Some interesting properties can be like: At the end of ith iteration, a[0:i] is sorted, which when extended to i=100, results in the whole array being sorted.

Loop Invariant for your case: a[100-i: 100-1] is sorted

Обратите внимание, что когда я равняюсь 100, приведенное выше утверждение будет означать, что весь массив отсортирован, и это то, что вы хотите быть верным в конце алгоритма.

PS: только что понял, что это старый вопрос, в любом случае помогает улучшить мои навыки ответа:)

Answer 4

Ваша петля контролируется тестом i < 100, В теле цикла, i используется в нескольких местах, но назначается только в одном месте. Назначение всегда происходит, и для любого значения i который разрешает вход в цикл, назначение будет сходиться к завершающему условию. Таким образом цикл гарантированно завершится.

Что касается правильности вашей программы, это другая проблема. В зависимости от того, используют ли ваши массивы индексацию с нуля или на основе единицы, способ использования i доступ к массиву может быть проблематичным. Если он основан на нуле, вы никогда не смотрите на первый элемент и выходите за пределы a[i+1] на последней итерации.