Почему программы не могут быть доказаны? - PullRequest
58 голосов
/ 25 января 2009

Почему компьютерная программа не может быть доказана так же, как математическое утверждение? Математическое доказательство построено на других доказательствах, которые построены от еще большего количества доказательств и вплоть до аксиом - тех истин истин, которые мы считаем самоочевидными.

Компьютерные программы, похоже, не имеют такой структуры. Если вы пишете компьютерную программу, как получается, что вы можете взять предыдущие проверенные работы и использовать их, чтобы показать истинность вашей программы? Вы не можете, так как ничего не существует. Далее, каковы аксиомы программирования? Самые атомные истины поля?

У меня нет хороших ответов на вышесказанное. Но кажется, что программное обеспечение не может быть доказано, потому что это искусство, а не наука. Как ты докажешь Пикассо?

Ответы [ 31 ]

0 голосов
/ 25 января 2009

подтверждение правильности программы может быть сделано только относительно спецификации программы; это возможно, но дорого / трудоемко

некоторые системы CASE создают программы, более поддающиеся доказательствам, чем другие, - но опять же, это опирается на формальную семантику спецификации ...

... и как вы можете доказать правильность спецификации? Правильно! С большим количеством спецификаций!

...