Методы и средства инженерии программного обеспечения


         

Методы доказательства программ


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

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

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

К методам проверки правильности программ относятся:

1)  методы доказательство правильности программ;

2)  верификация и аттестация программ.




Содержание  Назад  Вперед