Методы доказательства программ
Формальное математическое доказательство основывается на аксиомах, а сам процесс основывается на спецификации описания алгоритма доказываемой программы.
Доказательство корректности начинается с предположения о том, что в начале работы программы удовлетворяются некоторые условия, называемые предварительными условиями или предусловиями. Для проведения доказательства разрабатываются утверждения
о правильности выполнения операторов программы в различных точках программы. Создается набор утверждений, каждое из которых является следствием предусловий и последовательности инструкций, приводящих к соответствующей отмеченной точке программы, для которой сформулировано данное утверждение. Если утверждение соответствует конечному оператору программы, то выполняется заключительное утверждение и пост условие, позволяющее сделать вывод (заключение) о правильности работы программы [5, 8–11].
К методам проверки правильности программ относятся:
1) методы доказательство правильности программ;
2) верификация и аттестация программ.
