Инвариант цикла и ограничивающая функция

Правило верификации для оператора цикла:

" Если {P and B} S {P}, то.

{P} while B do S {P and not B}" .

Правило вводит важное понятие инварианта цикла.

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

Построим следующее утверждение относительно цикла while:

{ P }.

while P and B do S;

{ P and not B }.

Явное указание инварианта P для цикла представляет наибольшую ценность в программной документации и помогает избежать многих ошибок, которые могут быть выявлены только посредством тщательного тестирования.

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

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

P and not B => R, где R — постусловие.

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

Второй важный принцип при построении цикла — это завершение цикла (проблема останова). Чтобы показать, что выполнение цикла завершится, вводится целочисленная функция t (t>0), определенная на значениях переменных программы. Эта функция является верхней границей числа шагов цикла (ограничивающая функция). При каждом шаге цикла t уменьшается до тех пор, пока выполнение цикла не завершилось.

Тело цикла следует строить таким образом, чтобы оно уменьшало ограничивающую функцию при сохранении истинности инварианта P.

Для того чтобы понять, правильно ли построен цикл, достаточно проверить следующий список условий:

• 1) P истинно перед выполнением цикла;
• 2) выполнение цикла завершится при истинном значении P;
• 3) в момент завершения цикла истинен искомый результат, то есть

P and not B => R;

• 4) t ограничена снизу (t > 0) до тех пор, пока цикл не завершится;
• 5) каждый шаг цикла приводит к уменьшению ограничивающей функции t.