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