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