Правильность программы, спецификация

17

Из Википедии: В теоретической информатике правильность алгоритма утверждается, когда говорят, что алгоритм корректен по отношению к спецификации.

Но проблема в том, что получить «подходящую» спецификацию - это не тривиальная задача, и нет 100% правильного метода (насколько я знаю), чтобы получить правильный, это просто оценка, поэтому, если мы собираемся принять предикат в качестве спецификации только потому, что он «выглядит» как «один», почему бы не принять программу как правильную только потому, что она «выглядит» правильно?

Майкель Джаксон
источник
2
Потому что, надеюсь, спецификация менее сложна, чем программа, поэтому в ней будет меньше ошибок, чем в программе.
user253751
1
Обратите внимание, что система типов является формой спецификации - мы можем использовать ее для доказательства некоторых нетривиальных свойств программ. Чем богаче система типов, тем сильнее свойства, которые мы можем доказать.
садовод
@immibis, но если в нем только одна ошибка, значит, все не так
Мэйкел Джаксон
@MakelJakson Верно ... Однажды я ошибочно поставил противоречие в аксиоме Родена (то, что я пытался сделать, было правильным, но синтаксис был неправильным). Мне потребовалось некоторое время, чтобы «хммм, как мне кажется, авто-прувер сейчас работает необычайно хорошо», прежде чем я заметил.
user253751

Ответы:

30

Во-первых, вы абсолютно правы: вас интересует настоящее дело. Формальная проверка переносит проблему уверенности в правильности программы в проблему уверенности в правильности спецификации, поэтому это не серебряная пуля.

Однако есть несколько причин, по которым этот процесс все еще может быть полезен.

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

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

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

  4. Спецификации могут меняться реже, чем код. Без формальных методов каждый раз, когда мы обновляем исходный код, мы должны вручную проверять, что обновление не будет содержать ошибок или недостатков. Формальные методы могут потенциально уменьшить эту нагрузку: предположим, что спецификация не меняется, поэтому обновления программного обеспечения включают только изменения в коде, а не изменения в спецификации. Затем для каждого обновления вы освобождаетесь от необходимости проверять, верна ли спецификация (она не изменилась, поэтому нет риска появления новых ошибок в спецификации), а также от необходимости проверять, является ли код все еще действующим. правильно (программа проверки проверяет это для вас). Вам все еще нужно проверить правильность исходной спецификации, но вам не нужно постоянно проверять ее каждый раз, когда разработчик вносит новый патч / обновление / изменение.

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

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

Вам также может понравиться Формальная проверка программ на практике, и почему мы не проводим больше исследований в отношении гарантий времени компиляции? для большего количества перспектив с некоторым отношением к этому.

DW
источник
Кроме того, по мере того, как спецификация становится более подробной, возрастает вероятность того, что она может быть записана в виде псевдокода. Используя ваш пример сортировки, более подробная версия «выходные данные должны быть в порядке возрастания» будет «каждое целое число в выходных данных, после первого должно быть больше, чем предыдущее число». Это, в свою очередь, может быть легко записано как что-то вроде for each integer I<sub> N</ sub> in set S (where N > 1) { assert I<sub> N</ sub> > I<sub> N - 1</ sub> }. Не уверен на 100% в обозначениях.
Джастин Тайм - Восстановить Монику
Таким образом, хорошая спецификация также может помочь создать код, а не просто проверить его.
Джастин Тайм - Восстановить Монику
1
Очевидный способ выполнить спецификацию сортировки состоит в том, чтобы перечислить все перестановки ввода и выбрать упорядоченную. Проблема с этим , однако, должна быть ясна ...
Дерек Элкинс покинул SE
19

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

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

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

Фактически, такая сложная система, как автопилот, имела бы несколько уровней спецификаций с разным количеством уточнений. При проектировании часто используется уточняющий подход: начните с некоторых свойств высокого уровня, таких как «автомобиль не упадет в стену», затем выясните, что для этого требуются датчики и тормоза, и определите некоторые основные требования к датчикам, тормозам. и пилотное программное обеспечение, а затем снова уточнить эти базовые требования при проектировании компонента (для датчика мне понадобится радар, DSP, библиотека обработки изображений и т. д.) и т. д. В процессе формальной разработки, доказано, что каждый уровень спецификации соответствует требованиям, установленным уровнем выше него, от свойств самого высокого уровня до кода.

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

¹ Противоположностью полностью формального подхода является «я думаю, это работает, но я не уверен». Когда вы ставите на это свою жизнь, это не так уж и здорово.

Жиль "ТАК - перестань быть злым"
источник
Можно ли доказать только одно свойство моего кода и убедиться, что оно всегда будет правильным, например, я просто хочу доказать, что индекс массива никогда не выходит за пределы массива, и мне все равно другие вещи?
Майкель Джексон
5
@MaykelJakson Конечно! Вы просто используете это как свою спецификацию. Возможно, это слабая спецификация, но ничто не мешает вам использовать это и использовать формальные методы, чтобы доказать это.
Чи