Вычислительная сложность «настоящих» компьютерных программ

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

Однако я не уверен, в какой степени это относится к реальным программным операциям, таким как операционные системы. Нуждаются ли эти типы программ в полной силе полноты по Тьюрингу? Существуют ли более простые модели вычислений (например, PR), в которых эти приложения могут быть написаны? Если да, то в какой степени это позволяет разрешить правильность программы?

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

Тем не менее, наивные ограничения на модель вычислений на самом деле не очень помогают в повышении практичности анализа программ. Причина в том, что вы можете получить программы, которые делают "почти то же самое", поворачивая циклы while

while P do 
   C

в циклы for с большой константой итерации:

for i = 0 to BIGNUM do 
  if P then 
    C
  else
    break

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

$\epsilon_0$

Поскольку вы спрашивали о корректности программ в реальных программах, таких как операционные системы, вас может заинтересовать проект seL4 ( журнал , pdf , конференция ).

Команда NICTA взяла микроядро третьего поколения из 8700 строк C и 600 строк ассемблера, реализованных в соответствии с абстрактной спецификацией на Haskell. Они предоставили формальное, проверенное машиной доказательство (в Изабель / HOL), что реализация строго следует спецификации. Это доказывает, что их программа не содержит ошибок.

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

Вопросы, которые вы задаете, на самом деле совсем другие.

Однако я не уверен, в какой степени это относится к реальным программным операциям, таким как операционные системы. Нуждаются ли эти типы программ в полной силе полноты по Тьюрингу?

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

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

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

В частности, вы можете изменить исходный вопрос на

Есть ли абстракция моего программного обеспечения, которую я могу эффективно анализировать в полной модели, не связанной с Тьюрингом?

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

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