Станут ли когда-нибудь доказательства корректности кода мейнстримом?[закрыто]

Question

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

Answer 1

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

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

Answer 2

Все, кроме самых тривиальных программ

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

Здесь я нашел хорошую статью на эту тему:

http://www.encyclopedia.com/doc/1O11-programcorrectnessproof.html

Answer 3

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

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

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

Answer 4

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

Spec# http://research.microsoft.com/en-us/projects/specsharp/Это расширение C#, которое поддерживает контракты с кодом (условия до/post и инварианты) и может использовать эти контракты для выполнения различных типов статического анализа.

Аналогичные проекты существуют для других языков, таких как JML для Java, и Eiffel имеет это в значительной степени встроено.

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

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

Answer 5

Нет, если не возникает метод автоматического доказательства кода без обширной работы разработчика.

Answer 6

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

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

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

Answer 7

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

Промышленное применение Astrée

Доказательство отсутствия RTE в системе, используемой Airbus с более чем 130 тыс. Линий кода в 2003 году, не кажется плохим, и мне интересно, будет ли кто -нибудь скажет, что это не реальный мир.

Answer 8

Нет. Общая пословица для этого является: «Теория, теория и практика одинаковы. На практике нет».

Один очень простой пример: опечатки.

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

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

Answer 9

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

Answer 10

Это уже используется всеми. Каждый раз, когда вы используете проверку типа вашего языка программирования, вы в основном делаете математическое доказательство правильности вашей программы. Это уже очень хорошо работает - это просто требует выбора правильных типов для каждой функции и структуры данных, которую вы используете. Чем точнее тип, тем лучше вы получите. Существующие типы, доступные на языках программирования, уже имеют достаточно мощные инструменты, чтобы описать практически любое возможное поведение. Это работает на каждом доступном языке. C ++ и статические языки просто делают чеки во время компиляции, в то время как более динамические языки, такие как Python, делают это при запуске программы. Проверка все еще существует на всех этих языках. (Например, C ++ уже поддерживает проверку побочных эффектов так же, как это делает Haskell, но вам просто нужно выбрать его использовать.)