Общая характеристика формальных методов доказательства
Над этим направлением работали многие теоретики–программисты, некоторые из них, которые являются базовыми методами доказательства программ, кратко излагаются ниже.
Метод Флойда основан на определении условий для входных и выходных данных и в выборе контрольных точек в доказываемой программе так, чтобы путь прохождения по программе проходил хотя бы через одну контрольную точку. Для этих точек формулируются утверждения о состоянии переменных в этих точках (для циклов эти утверждения должны быть истинными при каждом прохождении цикла – инварианты цикла).
Каждая точка рассматривается, как индуктивное утверждение, т.е формула, которая остается истинной при возвращении в эту точку программы и зависит не только от входных и выходных данных, но от значений промежуточных переменных. На основе индуктивных утверждений и условий на аргументы программы строятся условия проверки правильности этой программы. Для каждого пути программы между двумя точками устанавливается соответствие условий правильности и определяется истинность этих условий при успешном завершении программы на данных, которые удовлетворяют входным условиям.
Формирование таких утверждений оказалось очень сложной задачей, особенно для программ с высокой степенью параллельности и взаимодействия с пользователем. Как оказалось на практике, достаточность таких утверждений трудно проверить.
Доказательство корректности применялось для уже написанных программ и тех, что разрабатываются путем последовательной декомпозиции задачи на подзадачи, для каждого из них формулировалось утверждение с учетом условий ввода и вывода и соответствующих входных и выходных утверждений. Доказать истинность этих условий – основа метода доказательства полноты, однозначности и непротиворечивости спецификаций.
Метод Хоара – это усовершенствованный метод Флойда, основанный на аксиоматическом описании семантики ЯП исходных программ. Каждая аксиома описывает изменение значений переменных с помощью операторов этого языка.
Операторы перехода, рассматриваемый как выход из циклов и аварийных ситуаций, и вызовов процедур определяются правилами вывода, каждое из которых задает индуктивное высказывание для каждой метки и функции исходной программы Система правил вывода дополняется механизмом переименования глобальных переменных, условиями на аргументы и результаты.
Метод рекурсивных индукций Дж. Маккарти состоит в структурной проверке функций, работающих над структурными типами данных, изменяет структуры данных и диаграммы перехода во время символьного выполнения программ. Тестовая программа получает детерминированное входное состояние при вводе данных и условий, которое обеспечивает фиксацию переменных и изменение состояния.
Выполняемая программа рассматривается как серия изменений состояний, самое последнее состояние считается выходным состоянием и если оно получено, то программа считается правильной. Моделирование выполнения кода является дорогим процессом, обеспечивающим высокое качество исходного кода.
Метод Дейкстры включает два подхода к доказательству правильности программ. Первый – основан на модели вычислений, оперирующих с историями результатов вычислений при работе программ и анализом выполнения модели вычислений.
Второй подход базируется на формальном исследовании текста программы с помощью предикатов первого порядка применительно к классу асинхронных программ, в которых возникают состояния при выполнении операторов. В конце выполнения программы уничтожаются накопленные отработанные состояния программы. Основу этого метода составляет – перевычисление, математическая индукция и абстракция.
Перевычисление базируется на инвариантах отношений, которые проверяют границы вычислений в проверяемой программе. Математическая индукция применяется для проверки циклов и рекурсивных процедур с помощью необходимых и достаточных условий повторения вычислений. Абстракция
задает количественные ограничения, которые накладываются методом перевычислений.
Доказательство программ по данному методу можно рассматривать как доказательство теорем в математике, используя аппарат математической индукции при неформальном доказательстве правильности, который может привести к ошибкам, как в самом аппарате, так и в программе.
В общем метод математической индукции разрешает доказать истинность некоторого предположения Р(n), в зависимости от параметра n, для всех n ³ n0, и тем самым доказать случай Р (n0). Истинность Р(n) для любого значения n, доказывает Р(n+1) и тем самым доказательство истинности Р(n) для всех n ³ n0.
Этот путь доказательства используется для утверждения А относительно программы, которая при своем выполнении достигает определенной точки. Проходя через эту точку n раз, можно получить справедливость утверждения А(n), если докажем:
1) что справедливо А(1) при первом проходе через заданную точку,
2) если справедливо А(n) (при n–проходах через заданную точку), то справедливо и А (n+1) при прохождении через заданную точку n+1 раз.
Чтобы доказать, что некоторая программа правильная, надо правильно описать, что эта программа делает, т.е ее логику. Такое описание называется правильным высказыванием или просто утверждением. Исходя из предположения, при котором работающая программа в конце концов успешно завершится, утверждение о правильности будет справедливо.
