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

Question

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

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

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

Answer 1

Доказательства являются программами.

Официальная проверка программ - это огромная область исследований. (См., Например, группа в Карнеги-Меллон .)

Многие сложные программы были проверены; например, посмотрите это ядро, написанное на Haskell .

Answer 2

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

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

Вы должны прочитать Дисциплину программирования Дийсктра .

Затем вы должны прочитать «1013 * Наука программирования» Гриса .

Тогда вы будете знать, как доказать правильность программ.

Answer 3

Просто небольшой комментарий для тех, кто поднял неполноту - это не относится к всем аксиоматическим системам, только достаточно мощным системам.

Другими словами, Годель доказал, что аксиоматическая система, достаточно мощная, чтобы описать себя, обязательно будет неполной. Однако это не означает, что это будет бесполезно, и, как другие связывают с этим, были предприняты различные попытки доказательства программы.

Двойная проблема (написание программ для проверки доказательств) также очень интересна.

Answer 4

Проблема остановки показывает только то, что существуют программы, которые невозможно проверить. Гораздо более интересный и более практичный вопрос заключается в том, какой класс программ можно формально проверить. Может быть, любая программа, которая кого-то волнует, может (в теории) быть проверена На практике, пока что только очень маленькие программы оказались правильными.

Answer 5

На самом деле вы можете писать корректно правильные программы. Microsoft, например, создала расширение языка C # под названием Spec # , которое включает в себя автоматическую проверку теорем. Для java существует ESC / java . Я уверен, что есть еще много примеров.

( edit : очевидно, spec # больше не разрабатывается, но инструменты контракта станут частью .NET 4.0 )

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

Answer 6

Если вы действительно интересуетесь этой темой, позвольте мне сначала порекомендовать «Науку программирования» Дэвида Гриса, классическую вводную работу по этой теме.

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

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

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

Answer 7

Во-первых, почему вы говорите "программы НЕ ДОЛЖНЫ быть доказаны"?

Что вы подразумеваете под "программами"?

Если под программами вы имеете в виду алгоритмы, разве вы не знаете Крускала? Дейкстры? MST? Прима? Бинарный поиск? Сортировка слиянием? DP? У всех этих вещей есть математические модели, которые описывают их поведение.

ОПИСАНИЕ. Математика не объясняет почему вещей, она просто рисует картину того, как. Я не могу доказать вам, что Солнце завтра взойдет на Востоке, но я могу показать данные, где оно делало это в прошлом.

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

Подождите? Вы не можете? http://en.wikipedia.org/wiki/Algorithm#Algorithmic_analysis

Я не могу показать вам «правду» в программе так же, как я не могу показать вам «правду» на языке. Оба являются представлениями нашего эмпирического понимания мира. Не на "правде". Оставляя в стороне все тарабарщины, я могу математически продемонстрировать вам, что алгоритм сортировки слиянием будет сортировать элементы в списке с производительностью O (nlogn), что Dijkstra найдет кратчайший путь на взвешенном графе или что алгоритм Евклида найдет вас наилучшим общий делитель между двумя числами. «Правда в моей программе» в последнем случае, возможно, в том, что я найду для вас самый большой общий делитель между двумя числами, не так ли?

С помощью уравнения повторения я могу описать, как работает ваша программа Фибоначчи.

А компьютерное программирование - это искусство? Я уверен, что это так. Столько, сколько математика.

Answer 8

Я не из математики, поэтому простите мое невежество, но что значит «доказать программу»? Что ты доказываешь? Правильность? Корректность - это спецификация, которую программа должна подтвердить на «правильность». Но эта спецификация определяется человеком, и как вы проверяете правильность этой спецификации?

На мой взгляд, в программе есть ошибки, потому что людям трудно выразить то, что они действительно хотят. альтернативный текст http://www.processdevelopers.com/images/PM_Build_Swing.gif

Так что вы доказываете? Ошибки, вызванные отсутствием внимания?

Answer 9

Далее, каковы аксиомы программирования? Самые атомные истины в области?

Я изучил курс под названием «Контрактное программирование» (домашняя страница курса: http://www.daimi.au.dk/KBP2/). Вот что я могу экстраполировать из курса (и других курсов, которые я прошел)

Вы должны формально (математически) определить семантику вашего языка. Давайте подумаем о простом языке программирования; тот, который имеет только глобальные переменные, int, массивы int, арифметику, if-then-else, while, assignment и ничего не делать [вы, вероятно, можете использовать подмножество любого основного языка в качестве «реализации» этого].

Состояние выполнения - это список пар (имя переменной, значение переменной). Прочитайте «{Q1} S1 {Q2}», поскольку «оператор выполнения S1 переводит вас из состояния выполнения Q1 в состояние Q2».

Тогда одна аксиома будет "if both {Q1} S1 {Q2} and {Q2} S2 {Q3}, then {Q1} S1; S2 {Q3}". То есть, если оператор S1 переводит вас из состояния Q1 в Q2, а оператор S2 переводит вас из Q2 в Q3, то «S1; S2» (за S1 следует S2) переводит вас из состояния Q1 в состояние Q3.

Другая аксиома была бы "if {Q1 && e != 0} S1 {Q2} and {Q1 && e == 0} S2 {Q2}, then {Q1} if e then S1 else S2 {Q2}".

Теперь немного уточнений: Qn в {} на самом деле будут утверждениями о состояниях, а не о самих состояниях.

Предположим, что M (out, A1, A2) - это оператор, который выполняет слияние двух отсортированных массивов и сохраняет результат в out, и что все слова, которые я использую в следующем примере, были выражены формально (математически). Тогда "{sorted(A1) && sorted(A2)} A := M(A1, A2) {sorted(A) && permutationOf(A, A1 concatened with A2)}" - это утверждение, что М правильно реализует алгоритм слияния.

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

Надеюсь, это немного проиллюстрирует, как могут выглядеть корректные программы проверки. И поверьте мне: требуется 1026 * много работы, даже для казалось бы простых алгоритмов, чтобы доказать их правильность. Я знаю, я прочитал много попыток; -)

[если вы читаете это: ваша сдача прошла нормально, это все остальные, которые вызывали у меня головные боли; -)]

Answer 10

Конечно, могут, как и другие.

Доказательство правильности очень маленькой подпрограммы - это хорошее упражнение, которое ИМХО должен дать каждому студенту в программе, связанной с программированием, . Это дает вам глубокое понимание того, как сделать ваш код понятным, легко проверяемым и поддерживаемым.

Однако в реальном мире оно имеет ограниченное практическое использование.

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

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

Я бы порекомендовал найти классическую статью Брукса " No Silver Bullet ".