Характеристика базовых методов доказательства

Наиболее известными формальными методами доказательства программ являются метод рекурсивной индукции или индуктивных утверждений Флойда, метод структурной индукции Хоара, метод рекурсивных индукций Маккарти и др.^[1]

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

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

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

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

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

Метод Хоара — это усовершенствованный метод Флойда, основанный на аксиоматическом описании семантики ЯП исходных программ. Каждая аксиома описывает изменение значений переменных с помощью операторов этого языка. Основное внимание уделяется формализации операторов перехода и вызовов процедур с помощью правил вывода, каждое из которых задает индуктивное высказывание для каждой метки (точки) и функции исходной программы.

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

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

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

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

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

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

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

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

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

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

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

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

Метод математической индукции позволяет доказать истинность некоторого предположения Р (п) в зависимости от параметра п для всех п>п₀

и тем самым доказать случай Р (п₀). Исходя из истинности Р (п) для любого значения п, доказывается Р (п + 1), что достаточно для доказательства истинности Р (п) для всех п > п₀.

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

• 1) что справедливо А ( 1) при первом проходе через заданную точку;
• 2) если справедливо А (п) (при и-проходах через заданную точку), то справедливо и А (п + 1) при прохождении через заданную точку п + 1 раз.

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

Проверка правильности программ — это автоматизированный метод Хоара в системе автоматизации — СПРУТ, основанный на системе проверки утверждений о программах на ЯП Паскаль.

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

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

• [1] См.: Лаврищева Е. At. Программная инженерия. Парадигмы, технологии и CASE-средства.