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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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