Блог

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

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

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

Почему это нельзя сделать?

Вот программа :

 accept integer i greater than 2
loop with k from 2 to 2*i
  is k prime?
    is 2*i-k prime?
      exit safely
end loop
do something nasty.
  

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

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

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

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

Это один из Святых Граалей вычислительной техники и математики, известный как проблема Entscheidungsproblem. Вы не собираетесь это решать. Самые яркие умы в обеих областях потратили на это много лет и доказали, что это невозможно решить. Когда nbt и Паскаль Куок сказали, что вы получите Нобелевскую премию и Филдса за это, они действительно имели это в виду.

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

Да, это возможно, несмотря на то, что говорят теоретики. Существует множество компаний, продающих продукты, которые делают именно то, что вы описываете, среди них Vericode, Coverity, Fortify, Klocwork и Grammatech.

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

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

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