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

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

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

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

Ответы [ 31 ]

0 голосов
/ 07 ноября 2009

Большинство ответов было сфокусировано на практике, и это нормально: на практике вам не нужны формальные проверки Но что в теории?

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

0 голосов
/ 07 мая 2009

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

Если у вас относительно небольшой / средний проект (скажем, 10K строк кода), то, вероятно, доказательства будут также 10k строк, если не длиннее.

Подумайте, если в программе могут быть ошибки, в доказательстве также могут быть "ошибки". Может быть, вам понадобятся доказательства для доказательства!

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

Пока доказательства будут читать люди, они, как правило, менее строгие, чем фактический код.

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

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

0 голосов
/ 27 апреля 2009

Как отмечали другие, (некоторые) программы действительно могут быть доказаны.

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

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

Однако есть некоторые вещи, которые могут быть (и были) более легко формализованы (и доказаны). Если вы хотя бы можете доказать, что ваша программа не потерпит крах, это уже что-то: -).

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

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

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

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

Я немного читал об этом, но есть две проблемы.

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

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

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

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

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

  • Проверка требует прохождения всех возможных ветвей (вызовов, ifs и interupts), что в расширенном программном коде имеет сверхкубическую временную сложность (следовательно, она никогда не завершится в течение разумного времени).
  • Некоторые методы программирования, либо путем создания компонентов, либо с помощью отражения, делают невозможным статическое прогнозирование выполнения кода (т. Е. Вы не знаете, как другой программист будет использовать вашу библиотеку, а компилятору трудно предсказать, как отражение в потребитель вызовет функциональность.

А это всего лишь некоторые ...

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

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

Являются ли коды операций"атомными истинами"? Например, увидев ...

mov ax,1

... не может программист утверждать, что он аксиоматичен, что, если исключить аппаратную проблему, после выполнения этого оператора регистр ax ЦП теперь будет содержать 1?

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

Тогда «предыдущая работа» может быть средой выполнения, в которой запускается новая программа.

Новая программа может быть доказана: кроме формальных доказательств, она может быть доказана «путем проверки» и различными формами «тестирования» (включая «приемочное тестирование»).

Как вы докажете Пикассо?

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

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

Если программа имеет четко определенные цель и исходные предположения (игнорируя Годеля ...), это может быть доказано. Найдите все простые числа x для 6 <= x <= 10, ваш ответ 7, и это можно доказать. Я написал программу <a href="http://www.astro.washington.edu/users/bastidas/codes/nim.py" rel="nofollow noreferrer">, которая воспроизводит NIM (первая программа на Python, которую я когда-либо писал), и теоретически компьютер всегда побеждает после того, как игра попадает в состояние, в котором компьютер может победить. Я не смог доказать, что это правда, но это правда (математически с помощью цифрового доказательства двоичной суммы), я верю, если я не допустил ошибку в коде. Я сделал ошибку, не серьезно, кто-то может сказать мне, если эта программа побиваемая?

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

0 голосов
/ 09 ноября 2011

Просто мои 2 цента, добавляя к интересным вещам уже там.

Из всех программ, которые не могут быть доказаны, наиболее распространенными являются те, которые выполняют ввод-вывод (некоторое непредсказуемое взаимодействие с миром или пользователями). Даже автоматические доказательства иногда просто забывают, что «проверенные» программы работают на некотором физическом оборудовании, а не в идеале, описанном моделью.

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

0 голосов
/ 10 июня 2012

С менее абстрактной точки зрения доказательство чего-либо - это вопрос уменьшения поля неопределенности до проверенного нулевого множества. Это желаемое за действительное, потому что в реальном мире просто невозможно достичь совершенства.

Компьютерная программа может быть достоверно верной и давать сбой в реальном мире, если ее среда не доказана (или не может быть доказана):

  • должны быть проверены ядро ​​ОС, драйверы и все библиотеки пользовательского режима и одновременно выполняемые программы, включая их прямые и косвенные краткосрочные и долгосрочные побочные эффекты,

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

  • конечные пользователи должны всегда вести себя как ожидалось (известный фактор «X»).

Автоматическое исправление ошибок реализовано в различных аппаратных компонентах (ОЗУ, дисках, контроллерах и т. Д.), Но, тем не менее, аппаратные сбои все еще случаются - возникают каскадные ошибки и / или сбои в ... provably correct программах.

И я даже не пытаюсь сделать эпилог о творчестве конечного пользователя ...

Итак, программа (правильно) с рейтингом provably correct не означает, что в реальной жизни она равна provably safe.

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

...