это подтверждение того, что семантика программы соответствует предъявляемым требованиям, изложенным в спецификации этой программы.
ЗАЧЕМ НУЖНА ПРОВЕРКА ПРАВИЛЬНОСТИ ПРОГРАММ?
1. Возрастание стоимости ущерба из-за пропущенной ошибки в программе.
4 июня 1996 года европейская космическая ракета «Ариан 5»
взорвалась менее чем через сорок секунд после запуска.
Комиссия, расследовавшая аварию, обнаружила, что ее причиной послужила ошибка в программе компьютера, отвечавшего за расчеты движения ракеты.
Аппаратные и программные системы широко используются во многих приложениях, где любой отказ считается недопустимым:
-
-
-
-