Почему программы нельзя доказать?
https://stackoverflow.com/questions/476959
-
20-08-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
RussianВопрос
Почему компьютерную программу нельзя доказать так же, как можно доказать математическое утверждение?Математическое доказательство строится на других доказательствах, которые строятся на основе еще большего числа доказательств и вплоть до аксиом — тех истин, которые мы считаем самоочевидными.
Компьютерные программы, похоже, не имеют такой структуры.Если вы пишете компьютерную программу, как вы можете взять предыдущие проверенные работы и использовать их, чтобы показать истинность вашей программы?Вы не можете, поскольку их не существует.Далее, каковы аксиомы программирования?Самые атомарные истины поля?
У меня нет хороших ответов на вышеизложенное.Но кажется, что программное обеспечение невозможно доказать, потому что это искусство, а не наука.Как доказать, что это Пикассо?
Решение
Доказательства являются программами.
Формальная проверка программ - это огромная область исследований. (См., Например, группу в Карнеги-Меллоне .)
Многие сложные программы были проверены; например, посмотрите это ядро, написанное на Haskell .
Другие советы
Программы абсолютно могут быть подтверждены. Паршивые программы сложно доказать. Для того, чтобы сделать это даже достаточно хорошо, вы должны разработать программу и доказательство, взявшись за руки.
Вы не можете автоматизировать доказательство из-за проблемы остановки. Однако вы можете вручную доказать постусловия и предварительные условия любого произвольного оператора или последовательности операторов.
Вы должны прочитать Дисциплину программирования Dijsktra .
Затем вы должны прочитать «Наука программирования» Гриса . / р>
Тогда вы будете знать, как доказать правильность программ.
Просто небольшой комментарий для тех, кто поднял неполноту - это не относится к всем аксиоматическим системам, только к достаточно мощным .
Другими словами, Годель доказал, что аксиоматическая система, достаточно мощная, чтобы описать себя, обязательно будет неполной. Это не означает, что это будет бесполезно, и, как другие связывают с этим, были предприняты различные попытки доказательства программы.
Двойная проблема (написание программ для проверки доказательств) также очень интересна.
На самом деле вы можете писать корректно правильные программы. Например, Microsoft создала расширение языка C # под названием Spec # . который включает в себя автоматическое доказательство теорем. Для Java существует ESC / java . Я уверен, что есть еще много примеров.
( изменить : очевидно, что spec # больше не разрабатывается, а инструменты контракта станут частью .NET 4.0 )
Я вижу несколько плакатов, размахивающих руками о проблеме остановки или теоремы о неполноте , которые предположительно препятствуют автоматической проверке программ. Это конечно не правда; эти проблемы просто говорят нам о том, что можно писать программы, которые не могут быть подтверждены как правильные или неправильные . Это не мешает нам создавать программы, которые являются доказуемо правильными.
Проблема остановки показывает только то, что существуют программы, которые невозможно проверить. Гораздо более интересный и более практичный вопрос заключается в том, какой класс программ можно официально проверить. Может быть, любая программа, которая кого-то волнует, может (теоретически) быть проверена. На практике до сих пор только очень маленькие программы оказались правильными.
Если вы действительно интересуетесь этой темой, позвольте мне сначала порекомендовать Дэвида Гриса " Наука программирования " ;, классическую вводную работу по этой теме.
На самом деле можно доказать программы в некоторой степени правильно. Вы можете написать предварительные условия и постусловия, а затем доказать, что с учетом состояния, соответствующего предварительным условиям, результирующее состояние после выполнения будет соответствовать постусловиям.
Однако, где это сложно, так это циклы. Для этого вам дополнительно необходимо найти инвариант цикла и для отображения правильного завершения необходимо найти функцию верхней границы на максимально возможном количестве итераций, оставшихся после каждого цикла. Вы также должны показать, что это значение уменьшается по крайней мере на одну после каждой итерации цикла.
Если у вас есть все это для программы, доказательство является механическим. Но, к сожалению, нет способа автоматически получить инвариантные и связанные функции для циклов. Человеческой интуиции достаточно для тривиальных случаев с небольшими петлями, но реально сложные программы быстро становятся неразрешимыми.
Во-первых, почему вы говорите, что «программы НЕ МОГУТ быть доказаны»?
Что вообще вы подразумеваете под «программами»?
Если под программами вы имеете в виду алгоритмы, разве вы не знаете алгоритм Краскала?Дейкстры?МСТ?Прим?Бинарный поиск?Сортировка слиянием?ДП?У всех этих вещей есть математические модели, описывающие их поведение.
ОПИСЫВАТЬ.Математика не объясняет, почему вещи, она просто рисует картину того, как.Я не могу доказать вам, что Солнце завтра взойдет на востоке, но я могу показать данные, где оно делало это в прошлом.
Вы сказали:«Если вы пишете компьютерную программу, как вы можете взять предыдущие проверенные работы и использовать их, чтобы показать истинность вашей программы?Вы не можете, поскольку их не существует»
Ждать?Ты НЕ МОЖЕШЬ?http://en.wikipedia.org/wiki/Algorithm#Algorithmic_anaанализ
Я не могу показать вам «истину» в программе так же, как я не могу показать вам «истину» в языке.Оба являются отражением нашего эмпирического понимания мира.Не на «правде».Отбросив всю тарабарщину, я могу математически продемонстрировать вам, что алгоритм сортировки слиянием сортирует элементы в списке с производительностью O(nlogn), что Дейкстра находит кратчайший путь на взвешенном графе или что алгоритм Евклида находит наилучший путь. общий делитель двух чисел.«Истина в моей программе» в последнем случае может быть в том, что я найду наибольший общий делитель между двумя числами, вы так не думаете?
С помощью рекуррентного уравнения я могу объяснить вам, как работает ваша программа Фибоначчи.
Итак, является ли компьютерное программирование искусством?Я уверен, что это так.Так же, как и математика.
Я не из математического прошлого, так что прости мое невежество, но что значит & доказать программу " имею в виду? Что ты доказываешь? Правильность? Корректность - это спецификация, которую программа должна проверить, чтобы она была & Quot; правильная & Quot ;. Но эта спецификация определяется человеком, и как вы проверяете правильность этой спецификации?
На мой взгляд, в программе есть ошибки, потому что людям трудно выразить то, что они действительно хотят. альтернативный текст http://www.processdevelopers.com/images/PM_Build_Swing.gif
Так что ты доказываешь? Ошибки вызваны отсутствием внимания?
Далее, каковы аксиомы программирования? Самые атомные истины в этой области?
Я изучил курс под названием «Контрактное программирование» (домашняя страница курса: http: // www.daimi.au.dk/KBP2/ ). Вот что я могу экстраполировать из курса (и других курсов, которые я прошел)
Вы должны формально (математически) определить семантику вашего языка. Давайте подумаем о простом языке программирования; тот, который имеет только глобальные переменные, int, массивы int, арифметику, if-then-else, while, assignment и do-nothing [вы, вероятно, можете использовать подмножество любого основного языка в качестве " реализация " ; этого].
Состояние выполнения - это список пар (имя переменной, значение переменной). Читать & Quot; {Q1} S1 {Q2} & Quot; & оператор выполнения S1 переводит вас из состояния выполнения Q1 в состояние Q2 ".
Тогда одной аксиомой будет "if both {Q1} S1 {Q2} and {Q2} S2 {Q3}, then {Q1} S1; S2 {Q3}". То есть, если оператор S1 переводит вас из состояния Q1 в Q2, а оператор S2 переводит вас из Q2 в Q3, то & Quot; S1; S2 Quot &; (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)}" - это утверждение, что М правильно реализует алгоритм слияния.
Можно попытаться доказать это, используя приведенные выше аксиомы (возможно, понадобится несколько других. Вам, вероятно, понадобится цикл, например).
Надеюсь, это немного проиллюстрирует, как могут выглядеть корректные программы. И поверьте мне: требуется много работы, даже для, казалось бы, простых алгоритмов, чтобы доказать их правильность. Я знаю, я прочитал много попыток; -)
[если вы читаете это: ваша сдача прошла нормально, это все остальные, которые вызывали у меня головную боль; -)]
Конечно, могут, как и другие.
Доказательство правильности очень маленькой подпрограммы - это хорошее упражнение, которое IMHO должен дать каждому студенту в программе, связанной с программированием, требуется . Это дает вам глубокое понимание того, как сделать ваш код понятным, легко проверяемым и обслуживаемым.
Однако в реальном мире оно имеет ограниченное практическое использование.
Во-первых, как и в программах есть ошибки, так и в математических доказательствах. Как доказать, что математическое доказательство действительно верно и не содержит ошибок? Ты не можешь И в качестве контрпримера, в любом количестве опубликованных математических доказательств были обнаружены ошибки, иногда спустя годы.
Во-вторых, вы не можете доказать, что программа верна, не имея «априори» однозначного определения того, что программа должна делать. Но любое однозначное определение того, что должна делать программа, - это программа. (Хотя это может быть программа на каком-то языке спецификации, для которого у вас нет компилятора.) Поэтому, прежде чем вы сможете доказать, что программа корректна, вы должны сначала иметь другую программу, которая эквивалентна и известна заранее. чтобы быть правильным. Так что QED все это бесполезно.
Я бы порекомендовал отыскать классическое " Без серебряной пули " статья Брукса.
Есть много исследований в этой области ... как уже говорили другие, конструкции внутри языка программы являются сложными, и это только усугубляется при попытке подтвердить или доказать для любых заданных входных данных.
Однако многие языки допускают спецификации, какие входные данные являются приемлемыми (предварительные условия), а также позволяют указывать конечный результат (почтовые условия).
К таким языкам относятся: B, событие B, Ada, fortran.
И, конечно же, существует множество инструментов, которые призваны помочь нам доказать определенные свойства программ. Например, чтобы доказать свободу тупиков, можно было бы перехватить их программу через SPIN.
Существует также множество инструментов, которые также помогают нам обнаруживать логические ошибки. Это можно сделать с помощью статического анализа (goanna, satabs) или фактического выполнения кода (gnu valgrind?).
Тем не менее, не существует единственного инструмента, который действительно позволил бы доказать всю программу, начиная с ее создания (спецификации), реализации и развертывания. Метод B подходит близко, но проверка его реализации очень и очень слабая. (Предполагается, что люди непогрешимы при переводе речи в имплентацию).
<Ч>В качестве примечания, при использовании метода B вы часто обнаруживаете, что строите сложные доказательства из меньших аксиом. (И то же самое относится и к другим доказательствам доказательств теорем).
Они могут. Я провел много-много часов в качестве первокурсника колледжа, делая корректность программы.
Причина, по которой это не практично на макроуровне, состоит в том, что написание доказательства программы, как правило, намного сложнее, чем написание программы. Кроме того, сегодня программисты стремятся создавать системы, а не писать функции или программы.
В микроуровне я иногда делаю это мысленно для отдельных функций и стараюсь упорядочить свой код, чтобы их было легко проверить.
Есть известная статья о программном обеспечении космического челнока. Они делают доказательства, или что-то эквивалентное. Это невероятно дорого и отнимает много времени. Этот уровень проверки может быть им необходим, но для любого типа компании-производителя программного обеспечения для потребителей или коммерческого использования ваш обед будет съеден конкурентом, который поставит решение на 99,9% за 1% от стоимости. Никто не собирается платить 5000 долларов за MS Office, который немного стабильнее.
Если вы ищете уверенности, альтернативой программам проверки является их тестирование.Это легче понять и можно автоматизировать.Он также допускает класс программ, для которых доказательства математически невозможны, как описано выше.
Прежде всего, никакие доказательства не могут заменить прохождение приемочных испытаний:*
Тот факт, что программа действительно делает то, что она говорит, не означает, что она делает то, что хочет от нее пользователь.
Пока не вы можете доказать, что то, что он говорит, это то, чего хочет пользователь.
- Затем вам придется доказать, что они действительно хотите, потому что, будучи пользователем, они почти наверняка не знают, чего хотят.и т. д.Доведение до абсурда.
*не говоря уже о юнит-тестах, тестах покрытия, функциональных, интеграционных и прочих видах тестов.
Надеюсь, это поможет вам на вашем пути.
Вы можете не только проверять программы, но и позволять своему компьютеру создавать программы из доказательств. См. Coq . Так что вам даже не нужно беспокоиться о возможности допустить ошибку в вашей реализации.
Теоремы Годеля несмотря на это ... Какой бы смысл ? Какой упрощенный & "Истины &" Вы хотели бы доказать? Что бы вы хотели извлечь из этих истин? Хотя я могу есть эти слова ... где практичность?
Программы МОГУТ быть проверены. Это легко, если вы пишете их на языке, например, Standard ML из Нью-Джерси (SML / NJ).
Ваше высказывание широко, поэтому оно ловит много рыбы.
Суть в том, что некоторые программы определенно могут быть проверены. Все программы могут не быть подтвержденными.
Вот тривиальный пример, который, как вы помните, является точно таким же доказательством, который разрушил теорию множеств в те времена: создайте программу, которая может определить, верна ли сама себя, и обнаружит ли она, что равен правильно, дать неправильный ответ.
Это G & # 246; теорема Дела, простая и понятная.
Но это не так проблематично, так как мы можем доказать много программ.
Допустим, чисто функциональный язык (например, Haskell). Побочные эффекты могут быть приняты во внимание на таких языках.
Чтобы доказать, что программа дает правильный результат, вам нужно указать:
<Ол>Этот набор спецификаций называется денотационная семантика . Они позволяют вам доказать причину программ, использующих математику.
Хорошая новость заключается в том, что & структура программ " (пункт 3 выше) и & структура математических множеств " очень похожи (модное слово topos или декартова замкнутая категория ), поэтому 1 / доказательства, которые вы делаете на математической стороне, легко переносятся в программные конструкции 2 / программы, которые вы пишете, легко показать математически правильными.
Читайте о проблеме остановки (которая заключается в том, что трудно доказать что-то простое) как то, завершается ли программа или нет). По сути, проблема связана с G & # 246; теорема Дела о неполноте.
Некоторые части программ можно доказать.Например, компилятор C#, который статически проверяет и гарантирует безопасность типов в случае успешного компиляции.Но я подозреваю, что суть вашего вопроса — доказать, что программа работает правильно.Многие (я не осмелюсь сказать, что большинство) алгоритмов могут быть доказаны корректными, но целая программа, вероятно, не может быть доказана статически по следующим причинам:
- Проверка требует прохождения всех возможных ветвей (вызовов, if и прерываний), что в расширенном программном коде имеет суперкубическую временную сложность (следовательно, она никогда не завершится в течение разумного времени).
- Некоторые методы программирования, либо путем создания компонентов, либо с использованием отражения, делают невозможным статическое предсказание выполнения кода (т.вы не знаете, как другой программист будет использовать вашу библиотеку, а компилятору сложно предсказать, как отражение в потребителе вызовет функциональность.
И это лишь некоторые...
Если в программе четко определены цель и исходные предположения (без учета Годеля ...), это можно доказать. Найдите все простые числа x для 6 & Lt; = x & Lt; = 10, ваш ответ 7, и это можно доказать. Я написал программу, которая воспроизводит NIM (первая программа на Python Я когда-либо писал), и теоретически компьютер всегда побеждает после того, как игра попадает в состояние, в котором компьютер может победить. Я не смог доказать, что это правда, но это правда (математически с помощью цифрового доказательства двоичной суммы), я верю, если я не допустил ошибку в коде. Я сделал ошибку, не серьезно, кто-то может сказать мне, если эта программа побиваемая?
Есть некоторые математические теоремы, которые были & подтверждены &. с компьютерным кодом, таким как теорема о четырех цветах . Но есть возражения, потому что, как вы сказали, вы можете доказать программу?
Далее, каковы аксиомы программирования? Самые атомные истины в этой области?
Являются ли коды операций & "атомными истинами &"? Например, увидев ...
mov ax,1
... не может ли программист утверждать, что он аксиоматичен, что, исключая проблему с оборудованием, после выполнения этого оператора регистр ax ЦП теперь будет содержать 1?
Если вы пишете компьютерную программу, как получается, что вы можете взять предыдущие проверенные работы и использовать их для демонстрации истинности вашей программы?
" предыдущая работа " тогда может быть среда выполнения, в которой запускается новая программа.
Новая программа может быть доказана: кроме формальных доказательств, она может быть доказана " проверкой " и различными формами " тестирования " (включая " приемочное тестирование ").
Как ты докажешь Пикассо?
Если программное обеспечение больше похоже на промышленный дизайн или проектирование, чем на искусство, то лучшим вопросом может быть &: как доказать, мост или самолет? "
подтверждение правильности программы может быть сделано только относительно спецификации программы; это возможно, но дорого / отнимает много времени
некоторые системы CASE создают программы, более поддающиеся доказательствам, чем другие, - но опять же, это опирается на формальную семантику спецификации ...
... и как доказать правильность спецификации? Правильно! С дополнительными характеристиками!
Я немного читал об этом, но есть две проблемы.
Во-первых, вы не можете доказать какую-то абстрактную вещь, называемую правильностью. Вы можете, если все настроено правильно, доказать, что две формальные системы эквивалентны. Вы можете доказать, что программа реализует набор спецификаций, и это проще всего сделать, построив доказательство и программу более или менее параллельно. Следовательно, спецификации должны быть достаточно подробными, чтобы можно было что-то доказывать, и поэтому спецификация фактически является программой . Проблема написания программы для достижения цели становится проблемой написания формальной подробной спецификации программы для достижения цели, и это не обязательно является шагом вперед.
Во-вторых, программы сложны. Так же как и доказательства правильности. Если вы можете ошибиться при написании программы, вы можете сделать одно доказательство. Дейкстра и Грис, по сути, сказали мне, что если бы я был идеальным математиком, я мог бы быть хорошим программистом. Ценность здесь в том, что доказательство и программирование - это два несколько разных мыслительных процесса, и, по крайней мере, по моему опыту, я допускаю разные виды ошибок.
По моему опыту, доказывающие программы не бесполезны. Когда я пытаюсь сделать что-то, что я могу описать формально, проверка правильности реализации устраняет множество трудно обнаруживаемых ошибок, в первую очередь оставляя тупые ошибки, которые я легко обнаруживаю при тестировании. В проекте, который должен генерировать чрезвычайно безошибочный код, это может быть полезным дополнением. Это не подходит для каждого приложения, и это, конечно, не серебряная пуля.
Как отмечали другие, (некоторые) программы действительно могут быть доказаны.
Однако на практике одна проблема заключается в том, что вам сначала нужно что-то (то есть предположение или теорема), которые вы хотите доказать. Таким образом, чтобы доказать что-то о программе, вам сначала необходимо получить формальное описание того, что она должна делать (например, до и после условия).
Другими словами, вам нужна формальная спецификация программы. Но получение даже разумной (а тем более строгой формальной) спецификации - это уже одна из самых сложных вещей в разработке программного обеспечения. Поэтому, как правило, очень трудно доказать интересные вещи о (реальной) программе.
Однако есть некоторые вещи, которые могут быть (и были) более легко формализованы (и доказаны). Если вы хотя бы можете доказать, что ваша программа не потерпит крах, это уже что-то: -).
Кстати, некоторые предупреждения / ошибки компилятора являются по существу (простыми) доказательствами программы. Например, компилятор Java докажет, что вы никогда не получите доступ к неинициализированной переменной в вашем коде (иначе это приведет к ошибке компилятора).
Я не прочитал все ответы, но, как я вижу, доказывать программы бессмысленно, поэтому никто не делает этого.
Если у вас относительно небольшой / средний проект (скажем, 10 тыс. строк кода), то, вероятно, доказательство будет также 10 тыс. строк, если не длиннее.
Подумайте, если в программе могут быть ошибки, в доказательстве также может быть " bugs " ;. Может быть, вам понадобится доказательство для доказательства!
Еще одна вещь, которую нужно учитывать, программы очень формальные и точные. Вы не можете быть более строгим и формальным, потому что программный код должен выполняться очень глупой машиной.
Хотя доказательства собираются читать люди, они, как правило, менее строгие, чем фактический код.
Единственное, что вы хотите доказать, это низкоуровневые алгоритмы, которые работают с конкретными структурами данных (например, быстрая сортировка, вставка в двоичное дерево и т. д.).
Эти вещи несколько сложны, не сразу понятно, почему они работают и / или будут ли они работать всегда. Они также являются основными строительными блоками для всего остального программного обеспечения.
Большинство ответов были сосредоточены на практике, и это нормально: на практике вам не нужны формальные проверки. Но что в теории?
Программы могут быть доказаны так же, как математическое утверждение. Но не в том смысле, в котором вы имели в виду! В любой достаточно мощной структуре есть математические утверждения (и программы), которые невозможно доказать! здесь
Здесь так много шума, но я все равно буду кричать на ветру ...
" доказать правильность " имеет разные значения в разных контекстах. В формальных системах , & Подтвердите правильность & Quot; означает, что формула может быть получена из других проверенных (или аксиоматических) формул. " доказать правильность " в программировании просто показывает, что код эквивалентен формальной спецификации. Но как доказать правильность формальной спецификации? К сожалению, нет способа показать, что спецификация не содержит ошибок или решает любую реальную проблему, кроме как через тестирование.
Просто мои 2 цента, добавляя к интересным вещам уже там.
Из всех программ, которые не могут быть доказаны, наиболее распространенными являются те, которые выполняют ввод-вывод (некоторое непредсказуемое взаимодействие с миром или пользователями). Даже автоматические доказательства иногда просто забывают, что & Quot; проверенный & Quot; & Программы Quot; работать на некотором физическом оборудовании, а не на идеальном, описанном моделью.
С другой стороны, математические доказательства не заботятся о мире. Повторяющийся вопрос с математикой, если он описывает что-то реальное. Он возникает каждый раз, когда изобретается что-то новое, например, воображаемые числа или неевклидово пространство. Тогда вопрос забывается, поскольку эти новые теории являются такими хорошими инструментами. Как хорошая программа, она просто работает.
