Модель доказательства корректности перестановки данных в векторе

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

Таблица 6.1

Логические операции.

¹ См.: Лаврищева Е. М. Программная инженерия. Парадигмы, технологии и CASEсредства., 2016. — 284 с.

Окончание табл. 6.1

Алгоритм программы состоит в построении для одномерного массива целых чисел Т длины N (array Т |1:Л^Г|) эквивалентного массива Г той же длины N, что и массив Г, и его элементы должны располагаться в порядке возрастания их значений. Иными словами, цель данного алгоритма — сортировка элементов исходного массива Т по их возрастанию. Доказательство правильности алгоритма сортировки элементов массива Т проведем с использованием ряда утверждений относительно элементов этого алгоритма, который описывается 111—116.

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

A_bcg: (Т 1: Л^г| — массив целых) & (Г[ 1: А] массив целых).

Выходное утверждение A_cnd запишем как конъюнкции таких условий:

• (а) (Г — массив целых) & (Г — массив целых);
• (б) (Vi, если i < N, то 3 j (Ti) < Г (/)));
• (в) (Vi, если г < ЛГ, го (Ti) < Г (i + 1)); т. е. A_end — это
• (Г — массив целых) & (Т — массив целых)

& Vi, если i < К то 3 j (Г (г) < ГО')).

& V/, если i < N., то (Г (г) < T'(i + 1)).

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

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

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

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

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

Так, оператор присваивания означает, что для всех i (i 0) выполняется (T'[i: = T[i]).

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

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

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

Оператор изменяет местами элементы массива.

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

которое является частью условия «в» утверждения Л_{еп (1} (для одной конкретной пары смежных элементов массива Т).

Очевидно также, что семантика оператора обмена местами не нарушает условие «б» выходного утверждения Л_{СП (1}.

Алгоритм выполняет всевозможные замены данных в каждой паре смежных элементов массива Г' за один проход через Г', т. е. оператор обмена работал один или больше раз. Однако пузырьковая сортировка не дает гарантии, что достигнуто упорядочение за один проход, но массиву Т', поскольку после очередного обмена индекс i увеличивается на единицу независимо от того, как соотносится новый элемент Тг) с предшествующим элементом Ti — 1).

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

Часть алгоритма, обозначенная точкой с двумя звездочками, выполняется до тех пор, пока не будет упорядочен весь массив, т. е. не будет выполняться условие «в» утверждения Л_{еП (} для всех элементов массива Т'

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

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

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

Если Л₃ — следующая точка преобразования, то второй теоремой будет: Л₂ —?>А₃

Таким образом, формулируется общая теорема: Л, —" Aj, где Л, и Л_;— — смежные точки преобразования.

Последняя теорема формулируется так, что условие, «истинное» в последней точке, отвечает истинности выходного утверждения: А_к —> Л_е11с|.

Следовательно, можно возвратиться потом к точке преобразования Л_{СП (}) и к предшествующей точке преобразования.

Доказали, что А_к —> Л_е11(1, а значит, верно Л_; —> Л, ₊₁ и т. д., пока не получим, что А_{ —> Л₀.

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

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

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