Теоретически безглючные программы

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

• Проблема остановки
• Теорема Гёделя о неполноте
• Теорема Райса

На самом деле теорема Райс выглядит как следствие проблемы остановки, и проблема остановки находится в тесной связи с теоремой Гёделя о неполноте.

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

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

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

Заметьте, не из-за отсутствия попыток. Системы типов должны обеспечивать определенную уверенность; У Haskell очень сложная система типов, которая в некоторой степени это делает. Но вы никогда не сможете устранить всю неопределенность.

Рассмотрим следующую функцию:

int add(int a, int b) { return a + b; }

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

LaunchMissiles();

вместо?

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

Я знаю, о чем ты думаешь. «Но я говорю о программном, а не аппаратном обеспечении».

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

Почему? Потому что у вас есть эти вещи, называемые крайними случаями.

И как только вы выходите за пределы простоты return a + b, становится чрезвычайно трудно доказать правильность программы.

Дальнейшее чтение
Они пишут правильные вещи
Взрыв Ariane 5

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

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

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

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

Неподтверждение - это интуитивное расширение проблемы остановки, в сочетании с данными наблюдений повседневного опыта.

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

Означает ли это, что каждая программа будет иметь по крайней мере одно непреднамеренное поведение?

Нет. Хотя в большинстве приложений обнаружена хотя бы одна ошибка или непреднамеренное поведение.

Или это означает, что невозможно написать код для проверки?

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

Для более подробной информации см. Coq - такой инструмент / язык / система.

Как насчет рекурсивной проверки?

Я не знаю. Я не знаком с этим, и я не уверен, если это проблема вычислимости или проблема оптимизации компилятора.

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

Правильные программы могут быть и написаны. Имейте в виде, программа может быть правильной, но это исполнение может произойти сбой из - за, например, физические обстоятельства (как пользователь Роберт Харви написал в своем ответе здесь ), но это отличается от того: Код этой программы по - прежнему верен. Точнее говоря, ошибка вызвана не ошибкой или ошибкой в самой программе, а в базовой машине, которая ее выполняет (*).

(*) Я заимствую определения для сбоя , ошибки и сбоя из поля надежности как, соответственно, статический дефект, неправильное внутреннее состояние и неправильное наблюдаемое поведение извне в соответствии с его спецификацией (см. <Любую статью из этого поля>) ,

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

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

Вы можете написать программу, которая проверяет правильность определенной X-программы. Например, если вы определяете программу «hello world» как программу с двумя последовательными инструкциями, а именно, print("hello world")и exitвы можете написать программу, которая проверяет, является ли ее входная программа программой, составленной из этих двух последовательных инструкций, и, таким образом, сообщает, является ли она правильная программа "привет мир" или нет.

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

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

Обычно эти варианты кодируются разными командами разработчиков с использованием разных компиляторов, а иногда выполняются на разных процессорах с разными ОС. Результаты оцениваются перед выводом пользователю. Боинг и Аэробус любят эту архитектуру.

Два слабых звена остаются, приводя к ошибкам общего режима:

• Есть только одна спецификация.
• Система голосования является уникальной или сложной.

Программа имеет некоторую спецификацию и работает в некоторой среде.

^{(пример космических лучей в других ответах изменяющимися addв FireMissiles можно думать часть «окружающей среды»)}

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

В частности, вы можете использовать анализаторы источника статического звука, например, Frama-C .

^{(но текущее состояние искусства таких анализаторов не позволяет весь анализ программы & доказательство крупномасштабных программ , такие как GCC компилятор или браузер Firefox или ядра Linux, и моя вера в то , что такие доказательства не будут происходить в моей жизни Я родился в 1959 году)}

Тем не менее, то, что вы доказали, - это правильное поведение программы по отношению к какой-то конкретной спецификации в некоторой (одной) среде (ах).

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

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

Читайте также записи в блоге Дж. Питра .

Кстати, проблема остановки или теорема Гёделя, вероятно, применима и к человеческому мозгу, или даже к человеческому виду.

Означает ли это, что каждая программа будет иметь по крайней мере одно непреднамеренное поведение?

Нет.

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

Теоремы Гёделя о неполноте имеют схожую с ними серую область. Учитывая математическую систему достаточной сложности, будут существовать некоторые утверждения, сделанные в контексте той системы, достоверность которой не может быть оценена. Это не означает, что математики должны отказаться от идеи доказательства. Доказательство остается краеугольным камнем математики.

Некоторые программы могут быть подтверждены. Это не легко, но это может быть сделано. Это цель формального доказательства теорем (часть формальных методов). Теоремы Гёделя о неполноте поражают: не все программы могут быть доказаны как правильные. Это не означает, что использовать формальные методы совершенно бесполезно, поскольку некоторые программы действительно могут быть формально доказаны как правильные.

Примечание. Формальные методы исключают возможность попадания космического луча в процессор и выполнения launch_missiles()вместо a+b. Они анализируют программы в контексте абстрактной машины, а не реальных машин, которые подвержены отдельным событиям, таким как космический луч Роберта Харви.

Здесь есть много хороших ответов, но все они, кажется, огибают критическую точку, которая заключается в следующем: все эти теоремы имеют схожую структуру и говорят схожие вещи, а то, что они говорят - нет, «невозможно написать правильно программы»(для некоторого конкретного значения„правильно“и„программа“ , которая варьируется в каждом отдельном случае), но то , что они делают слово„это невозможно предотвратить кого - то писать неверную программу , которую мы не можем оказаться неверным“( и т.д).

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

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

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

Код может быть без ошибок. Возьмите любой из примеров кода «Hello World» для любого языка программирования и запустите его на той платформе, для которой он предназначен, и он будет работать согласованно и давать желаемые результаты. Там заканчивается любая теория о невозможности кода без ошибок.

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

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

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

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

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

В реальных приложениях разработки программного обеспечения вы не сможете заставить их летать, объяснив бизнесу, почему теоретически приложения не могут быть безошибочными. Дискуссии такого рода между технологиями и бизнесом никогда не произойдут, за исключением тех случаев, когда произошла технологическая неисправность, которая повлияла на способность бизнеса зарабатывать деньги, предотвращать потерю денег и / или поддерживать жизнь людей. Ответ на вопрос «как это может произойти» не может быть «позвольте мне объяснить эту теорию, чтобы вы поняли».

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

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

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

Программирование является областью науки и математики, и в этом случае оба бесконечны. Главное в работе разработчика - наша работа бесконечна.

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

Так может ли код быть эффективным? Да.
Можно ли бесконечно оптимизировать код? Да.
Может ли код быть без ошибок? Нет, вы просто еще не нашли способ сломать это.
При этом, если вы стремитесь улучшить себя и свои методы написания кода, ваш код будет трудно сломать.