Они широко использовались в Macsyma, пользователи Macsyma все время с ними работали. И вот приходит сообщение от Билла Госпера: “Частное двух этих целых чисел неверно”. Он заметил это, поскольку частное примерно равнялось Юл.

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

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

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

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

Сейбел: Как обычно - ошибка не ходит одна.

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

Сейбел: Кроме ночных озарений, каков ваш излюбленный метод отладки? Что вы предпочитаете - символьные отладчики, вывод на печать, утверждения, формальные доказательства или все сразу?

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

И я полностью перешел на модульное тестирование. Пришлось придумывать модульные тесты для каждой из функций. Крайне полезный опыт.

Это повлияло на облик Fortress - я постарался ввести туда свойства, поощряющие модульное тестирование. И записать их не в отдельные файлы, а вместе с текстом программы. Мы заимствовали кое- что из контрактного программирования языка Eiffel - предусловия и постусловия для процедур. Есть места, где размещаются тестовые данные и процедуры модульных тестов, и тестовая программа запускает эти процедуры по первому вашему требованию.

Сейбел: Раз уж вы упомянули контрактное программирование: как вы используете утверждения в собственном коде?

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

Сейбел: А как насчет пошаговой отладки? Если все прочее не помогает, вы прибегаете к ней?

Стил: Зависит от длины программы. И, конечно, помогают инструменты, которые позволяют пропускать целые заведомо безошибочные куски. В Common Lisp есть отличная функция STEP. Я много раз пошагово отлаживал код на Common Lisp. Это очень здорово - возможность пропустить функции, в которых уверен. И еще возможность расставить ловушки и сказать себе: “Сюда мне смотреть не нужно, до тех пор пока этот цикл не повторится семнадцать раз”. На PDP-10 были для этого аппаратные средства, это было здорово, особенно в MIT. Тогда они любили модернизировать свои машины, добавляя в них что-нибудь. Можно долго рассказывать про выполнение одного и того же кода разными способами.

Сейбел: Вы применяете к своему коду формальные доказательства?

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

Сейбел: Питер ван дер Линден в своей книге “Expert С Programming” (Программирование на Си для экспертов) отвел доказательствам целую главу в пренебрежительном духе. Вот вам доказательство того-то, но смотрите - оно с ошибками! Ха-ха-ха!

Стил: Да, и доказательства могут быть с ошибками.

Сейбел: Но, по крайней мере, встретить ошибки в них меньше шансов, чем в проверяемом коде?

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

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

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

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

Вот один из самых интересных случаев в моей практике. Меня попросили написать отзыв на статью Дэвида Гриса для “САСМ”. Грис писал о доказательстве правильности параллельного алгоритма сборки мусора. Сьюзен Овицки была студенткой Гриса и разработала кое-какие инструменты для доказательства корректности параллельных программ. А Грис решил применить их к параллельному сборщику мусора, разработанному Дейкстрой. Код занимал где-то полстраницы. А остальная часть статьи содержала доказательство его корректности.

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

Сейбел: Итак, алгоритм содержал ошибки, и доказательство их пропустило.

Стил: Да, получилось, что доказательство некорректно. Что-то где-то было упущено. Какие-то детали работы с формулой - формула была почти правильна, но именно “почти”. Дело было лишь в том, чтобы поменять местами, например, две строки кода.

Сейбел: Итак, 25 часов ушло на то, чтобы проанализировать доказательство. Вы бы смогли найти ошибку в коде за 25 часов, имея перед собой только код и больше ничего?

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

Сейбел: И все выявилось в процессе доказательства, то есть вам не надо было рассматривать различные сценарии типа “что, если” для обнаружения проблемы.