Почему программы не могут быть доказаны?

Question

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

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

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

Answer 1

Что-то, что не было упомянуто здесь, это B-метод , который является формальной системой, основанной на методе. Он был использован для разработки системы безопасности парижского метро. Существуют инструменты для поддержки разработки B и Event B, в частности Rodin .

Answer 2

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

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

В микроуровне я иногда делаю это мысленно для отдельных функций и стараюсь упорядочить свой код, чтобы их было легко проверить.

Есть известная статья о программном обеспечении космического челнока. Они делают доказательства, или что-то эквивалентное. Это невероятно дорого и отнимает много времени. Этот уровень проверки может быть им необходим, но для любого типа компании-производителя программного обеспечения для потребителей или коммерческого использования ваш обед съедается конкурентом, который предлагает решение на 99,9% за 1% от стоимости. Никто не собирается платить 5000 долларов за MS Office, который немного стабильнее.

Answer 3

Вы можете не только проверять программы, но и позволять своему компьютеру создавать программы из доказательств. См. Coq . Так что вам даже не нужно беспокоиться о возможности допустить ошибку в вашей реализации.

Answer 4

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

Однако многие языки допускают спецификации, какие входные данные являются приемлемыми (предварительные условия), а также позволяют указывать конечный результат (почтовые условия).

К таким языкам относятся: B, Event B, Ada, fortran.

И, конечно, есть много инструментов, которые призваны помочь нам доказать определенные свойства программ. Например, чтобы доказать свободу тупиков, можно было бы перехватить их программу через SPIN.

Есть также много инструментов, которые также помогают нам обнаруживать логические ошибки. Это можно сделать с помощью статического анализа (goanna, satabs) или фактического выполнения кода (gnu valgrind?).

Тем не менее, не существует единственного инструмента, который действительно позволил бы доказать всю программу, начиная с ее создания (спецификации), реализации и развертывания. Метод B подходит близко, но проверка его реализации очень и очень слабая. (Предполагается, что люди непогрешимы в переводе speicficaiton на имплентацию).

---

В качестве примечания, при использовании метода B вы часто обнаруживаете, что строите сложные доказательства из меньших аксиом. (То же самое относится и к другим доказательным доказательствам теорем).

Answer 5

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

Прежде всего, никакие доказательства не могут заменить прохождение приемочных испытаний: *

• То, что программа действительно делает то, что говорит, не означает, что она делает то, что хочет от нее пользователь.

  • Если только вы не сможете доказать, что то, что он говорит, это то, что пользователь говорит, что он хочет.

    • То, что вы затем должны доказать, это то, чего они действительно хотят , потому что, будучи пользователем, они почти наверняка не знают, чего хотят. и т.д. Reductio ad absurdum.

* не говоря уже о модуле, покрытии, функционале, интеграции и всех других видах испытаний.

Надеюсь, это поможет вам на вашем пути.

Answer 6

Допустим, чисто функциональный язык (например, Haskell). Побочные эффекты могут быть приняты во внимание на таких языках.

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

1. соответствие между типами данных и математическими наборами
2. соответствие между функциями Haskell и математическими функциями
3. набор аксиом, определяющих, какие функции вам разрешено строить из других, и соответствующее конструирование на математической стороне.

Этот набор спецификаций называется денотационная семантика . Они позволяют вам доказать причину программ с использованием математики.

Хорошая новость заключается в том, что «структура программ» (пункт 3 выше) и «структура математических множеств» очень похожи (модное слово - topos или декартово замкнутая категория ), поэтому 1 / доказательства, которые вы делаете на математической стороне, будут легко перенесены в программные конструкции 2 / программы, которые вы пишете, легко показываются математически правильными.

Answer 7

Ваше высказывание широко, поэтому оно ловит много рыбы.

Суть в том, что некоторые программы определенно могут быть проверены. Все программы могут не быть подтвержденными.

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

Это теорема Геделя, простая и понятная.

Но это не так проблематично, поскольку мы можем доказать много программ.

Answer 8

Теоремы Гёделя несмотря на ... Какой в ​​этом смысл? Какие упрощенные «истины» вы хотели бы доказать? Что бы вы хотели извлечь из этих истин? Хотя я могу есть эти слова ... где практичность?

Answer 9

Программы МОГУТ быть проверены. Это легко, если вы пишете их на языке, например, Standard ML of New Jersey (SML / NJ).

Answer 10

Здесь так много шума, но я все равно буду кричать на ветру ...

«Докажи правильно» имеет разные значения в разных контекстах. В формальных системах «доказать правильность» означает, что формула может быть получена из других проверенных (или аксиоматических) формул. «Докажи правильно» в программировании просто показывает, что код эквивалентен формальной спецификации. Но как доказать правильность формальной спецификации? К сожалению, нет способа показать, что спецификация не содержит ошибок или решает любую реальную проблему, кроме как через тестирование.