Я думал о том, что мы можем доказать, что у программы есть ошибки. Мы можем проверить его, чтобы оценить, что он более или менее устойчив к ошибкам.Есть ли способ доказать, что программа не имеет ошибки?
Но есть ли способ (даже теоретически) доказать, что программа не имеет ошибки?
Для простых программ, таких как «Hello World», я думаю, мы сможем это сделать. Но как насчет более крупных программ?
В настоящее время существует множество различных формализмов, которые могут быть использованы для правильного отображения программ (например, формализации в помощниках-доказательствах, набираемых языков программирования, логики разделения, ...). Как отмечают другие, нет автоматического способа доказать правильность данной программы (см. Проблему остановки ). Однако упомянутые формализмы часто применимы к конкретным программам. (Такое приложение может быть далеко от автоматического и требует огромного количества творчества.)
Другим очень важным моментом является то, что мы на самом деле подразумеваем под доказав программу правильного или как вы заявили, доказать, что программа не имеет ошибки. Даже с формальными методами, как правило, нет способа сказать, что ничего не может пойти не так с программой. Причина в том, что формальные методы обычно показывают, что программа соответствует спецификации .
Вы можете представить спецификацию как логическую формулу (которая содержит некоторое свойство о программе) и доказательство корректности как формальное доказательство того, что программа удовлетворяет этой формуле (т. Е. Обладает соответствующим свойством). Из-за этой настройки все, что вне спецификации, даже не «считается» доказательством. Поэтому, чтобы действительно показать, что в программе нет ошибок, вам сначала нужно написать логическую формулу, которая указывает, когда в программе нет ошибок.
Таким образом, было бы более честным сказать, что формальные методы часто могут доказать (без сомнения), что в программе нет определенных видов ошибок (в зависимости от используемой спецификации).
Не в общем случае. Посмотрите на проблему с остановкой, которая является интуитивным доказательством того, что даже не представляется возможным написать программу, чтобы узнать, закончится ли другая программа, не говоря уже об ошибке. – RichieHindle
@RichieHindle Вы говорите, что невозможно корректно доказать правильность программ. Вопрос: «Есть ли способ доказать, что программа не имеет ошибки?» И ответ «да». Можно даже доказать довольно большую полезную программу: CompCert. И второй: seL4. –