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

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

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

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

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

o ,

o ,

o ,

т.е.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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