Кодеры за работой. Размышления о ремесле программиста
Шрифт:
Сейбел: То есть речь идет о средстве, встроенном в GDB, которое используется CWEB?
Кнут: И оно было встроено в GDB, потому что оно было встроено в Си, для того чтобы заполучить директивы__LINE__. Нам пришлось поработать, для того чтобы использовать директивы__LINE__, но теперь все работает превосходно. У компьютера есть только двоичная инструкция, но GDB знает, что это было получено из моего исходного WEB-файла, несмотря на то что WEB появился через 10 или 20 лет после Си. Следовательно, с их стороны было очень хорошим, дальновидным
Сейбел: То есть вы используете GDB. Какие еще инструменты отладки вы применяете?
Кнут: Я добавляю много кода, проверяющего качество исполнения моих структур данных, со всеми их повторами. Эта проверка достоверности, когда она включена, может замедлить выполнение программы на два порядка.
Например, у меня была сложная структура данных, в которой использовался подсчет ссылок. Я пишу довольно сложные программы, и процесс подсчета ссылок усложняется. Время от времени мне приходится то увеличивать, то уменьшать счетчик ссылок. Но когда указатель находится в регистре или является параметром подпрограммы, считается это ссылкой в структуре данных или нет? Поэтому я пишу проверку, которая проходит через миллион счетчиков, проверяя, сколько ссылок действительно было сделано и все ли сходится. Затем я делаю небольшие вычисления и проверяю все целиком. Таким образом, ошибки будут обнаружены за миллиард шагов до того, как они проявят себя и все рухнет.
Была одна программа, которая выполняла умножение с помощью нового способа, и я усиленно ее тестировал. Я составил ряд из 256 чисел и перемножил каждое с каждым, а после каждого шага делал проверку. Умножаю 2 на 3 — сбой! Исправляю. Потом еще что-нибудь. В конце концов я добрался до того момента, когда все 256 правильно умножались друг на друга.
Это очень важная техника отладки для меня. Наверное, около 10% кода посвящено тому, что мне нужно только во время отладки. Кроме того, код проверки также документирует структуру данных.
Кроме того, я обычно пишу программу, которая переводит структуру данных в удобную знаковую форму, чтобы избежать декодирования всего двоичного кода. Также при необходимости я могу распечатать структуру данных в хорошо организованной форме или скинуть ее в один файл и написать еще одну программу, которая проанализирует первую и найдет, что пошло не так.
Сейбел: Говоря об инвариантах и различных видах операторов утверждений, люди вроде Дейкстры говорят, что мы должны устанавливать очень формальные операторы утверждения на каждом этапе своих программ, чтобы в дальнейшем суметь доказать корректность этих программ. Я читал ваши рассуждения о том, что корректность программы нужно доказывать «неформально». Как вы думаете, стоит ли идти дальше и формально доказывать корректность программы?
Кнут: С одной стороны, невозможно что-либо доказать в принципе. Когда кто-то говорит, что его программа верифицирована, это значит, что она лишь соответствует неким критериям согласно результатам работы верификатора. Но в верификаторе может быть ошибка. Критерии могут быть неправильно сформулированы. Никогда нельзя с точностью
Самая первая работа Тони Хоара про формальное доказательство называлась «Proof of a Program: FIND (Доказательство программы: FIND). Это было прекрасное научное исследование, которое весьма продвинуло общее положение дел в этой области. Но в этом доказательстве было 2-3 ошибки. Тогда людям не приходило в голову проверять, находится ли список индексов внутри границ или еще что-нибудь в этом духе. Всегда есть опасность появления пробелов. Тем не менее он осуществил гораздо более качественную и тщательную проверку, чем кто-либо до него.
Или вот вчера я закончил программу и понятия не имею, как установить для нее все операторы утверждений. Мне это никогда не сделать, потому что я никогда не буду больше уверен в утверждениях, нежели в самой программе.
Или взять, к примеру, ТеХ — с формальной точки зрения там полный бардак. Задумывалось, что эту программу будут использовать люди, а не компьютеры. Было бы абсолютно невозможно сформулировать, что значит корректность для ТеХ. Некоторые методы формальной семантики настолько сложны, что никто не может внятно определить понятие корректности.
Сейбел: Работая над ТеХ, вы написали совершенно зубодробительный тест для программы.
Кнут: Верно.
Сейбел: Каким образом вам удается так относиться к своим программам? Программисты зачастую хотят защитить свое дитя, поэтому они, как правило, стараются не очень усердно тестировать свои программы.
Кнут: Я всю жизнь был придирчивым. И чтобы получить удовольствие от обнаружения ошибок, мне нужно просто забыть, что программу написал я сам. Я пытаюсь представить, что это чья-то чужая программа. В остальных же случаях мне достаточно легко переключиться в режим нападения. Не знаю почему.
Например, одно из моих лучших профессиональных достижений во время работы в Burroughs Corporation было связано с деятельностью по обнаружению ошибок в устройстве их аппаратного обеспечения. Их инженеры показывали мне спецификации для своих компьютеров, а мне нужно было сконструировать примеры, при которых они бы ошибались на единицу или что-то вроде того. Я нашел свыше 200 ошибок в их компьютерах серии В-5000, прежде чем они поступили в производство, хотя перед этим они прошли тест на эмуляторах.
Сейбел: То есть, по сути, вы изобретали программы, которые были верны с точки зрения семантики языка, но машина исполняла их некорректно?
Кнут: Да. Конечно же, если у них плавающая запятая неправильно вычисляла произведение двух чисел, я пытался найти примеры чисел, когда плавающая запятая не работала. Кроме того, иногда они реализовывали стек аппаратно, и у них были ситуации, когда регистры были пусты или не на верху стека, и я пытался придумать сценарии, в которых их логика не работала.