Доказательство конкретности с помощью утверждений

Рассмотрим формальное доказательство программы, заданной структурной логической схемой и совокупностью утверждений, задаваемых логическими операторами, комбинациями переменных (true/false), операциями (конъюнкция, дизъюнкция и др.) и кванторами всеобщности и существования (табл. 6.1).

Таблица 6.1. Список логических операций
Логические операции
Название	Примеры	Значение
Конъюнкция		и
Дизъюнкция		или
Отрицание		не
Импликация		если то
Эквивалентность		равнозначно
Квантор всеобщности		для всех , условие истинно
Квантор существования		существует , для которого истина

Цель алгоритма программы - построение для массива целых чисел длины эквивалентного массива той же длины , что и массив . Элементы в массиве должны располагаться в порядке возрастания их значений. Данный алгоритм реализуется сортировкой элементов исходного массива по их возрастанию. Доказательство правильности алгоритма сортировки элементов массива проводится с использованием ряда утверждений относительно элементов этого алгоритма, которые описываются пунктами П1- П6.

1. Входное условие алгоритма задается в виде начального утверждения:

Выходное утверждение - это конъюнкция таких условий:

o ,

o ,

o ,

т.е.

Расположение элементов массива в порядке возрастания их величин в массиве осуществляется алгоритмом пузырьковой сортировки, суть которого заключается в предварительном копировании массив в массив , а затем проводится сортировка элементов согласно условия их возрастания. Алгоритм сортировки представлен на блоксхеме (рис. 6.2).

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

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

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

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

Так, оператор присваивания означает, что для всех () выполняется (). Результат выполнения алгоритма в точке с нулем может быть выражен утверждением

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

увеличить изображение
Рис. 6.2. Схема сортировки элементов массива Т

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

В точке с одной звездочкой выполнен оператор который меняет местами элементы.

В результате работы оператора будет справедливым такое утверждение:

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

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

В этой точке также справедливо утверждение

Часть алгоритма, обозначенная точкой с двумя звездочками, выполняется до тех пор, пока не будет упорядочен весь массив, т.е. не будет выполняться условие в) утверждения для всех элементов массива .

Итак, выполнение исходных условий обеспечено порядком и соответствующей cемантикой операторов преобразования массива.

Доказано, что выполнение алгоритма программы завершено успешно, что означает ее правильность.

3. Этот алгоритм можно представить в виде серии теорем, которые доказываются. Начиная с первого утверждения и переходя от одного преобразования к другому, определяется индуктивный путь вывода. Если одно утверждение - истинно, то истинно и другое. Иными словами, если дано первое утверждение и первая точка преобразования , то первая теорема -

Если - следующая точка преобразования, то второй теоремой будет .

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

Следовательно, можно возвратиться к точке преобразования и к предшествующей точке преобразования. Доказав, что верно, значит, верно и и так далее, пока не получим, что .

4. Далее специфицируются утверждения типа - .

5. Чтобы доказать, что программа корректная, необходимо последовательно расположить все утверждения, начиная с и заканчивая , этим подтверждает истинность входного и выходного условий.

6. Доказательство алгоритма программы завершено.