Кодеры за работой. Размышления о ремесле программиста

Примером крайности в этой области может служить случай, имевший место, когда ТеХ адаптировался для работы с Unicode. У них был файл изменений раз в десять больше главной программы. Другими словами, из 8-битной программы они сделали 16-битную, но вместо того чтобы пройтись и переделать мою главную программу, они были настолько увлечены файлами изменений, что просто написали свои файлы изменений и назвали это Omega, - миллион строк файлов изменений для 20 000 строк кода ТеХ. Это крайность.

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

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

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

Затем я заменил это фразами вроде “Прочтем биты справа налево, а не слева направо - получится другая BDD” или “Попробуем все булевы функции от шести переменных, просмотрим их все и выясним, у которой из них наибольшая BDD”. Но это все лишь вариации моей исходной программы.

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

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

Кнут: Да, я пишу книгу.

Сейбел: Как по-вашему, этот механизм может получить более широкое применение?

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

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

Кнут: У меня теперь есть более эффективные инструменты для отладки в рамках литературного программирования - вот, по большому счету, и все.

Сейбел: Хорошо, давайте поговорим об отладке. Что это за более эффективные инструменты, которые вы сейчас используете?

Кнут: Как оказалось, изобретатели отладчика GNU поняли, что препроцессоры можно использовать для написания программ. То есть можно устанавливать соотношение между низкоуровневыми объектами и высокоуровневыми источниками в совершенно разных языках. Другими словами, я могу писать на CWEB, но никогда не смотреть на низкоуровневые вещи, потому что они отобразятся в моем CWEB-источнике по мере моего продвижения по программе.

Сейбел: То есть речь идет о средстве, встроенном в GDB, которое используется CWEB?

Кнут: И оно было встроено в GDB, потому что оно было встроено в Си, для того чтобы заполучить директивы__LINE__. Нам пришлось поработать, для того чтобы использовать директивы__LINE__, но теперь все работает превосходно. У компьютера есть только двоичная инструкция, но GDB знает, что это было получено из моего исходного WEB-файла, несмотря на то что WEB появился через 10 или 20 лет после Си. Следовательно, с их стороны было очень хорошим, дальновидным решением выполнить эту работу.

Сейбел: То есть вы используете GDB. Какие еще инструменты отладки вы применяете?

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

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

Была одна программа, которая выполняла умножение с помощью нового способа, и я усиленно ее тестировал. Я составил ряд из 256 чисел и перемножил каждое с каждым, а после каждого шага делал проверку. Умножаю 2 на 3 - сбой! Исправляю. Потом еще что-нибудь. В конце концов я добрался до того момента, когда все 256 правильно умножались друг на друга.

Это очень важная техника отладки для меня. Наверное, около 10% кода посвящено тому, что мне нужно только во время отладки. Кроме того, код проверки также документирует структуру данных.

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

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

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