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