Кодеры за работой. Размышления о ремесле программиста
Шрифт:
Сейбел: Раз уж вы упомянули контрактное программирование: как вы используете утверждения в собственном коде?
Стил: Обычно я вставляю утверждения преимущественно в начале процедур и в самых важных местах по всему коду. И пытаясь — «доказать», видимо, слишком сильное слово — убедить себя в правильности какого-то кода, я часто думаю в терминах инвариантов: слежу, чтобы инварианты поддерживались. Думаю, это плодотворный подход.
Сейбел: А как насчет пошаговой отладки? Если все прочее не помогает, вы
Стил: Зависит от длины программы. И, конечно, помогают инструменты, которые позволяют пропускать целые заведомо безошибочные куски. В Common Lisp есть отличная функция STEP. Я много раз пошагово отлаживал код на Common Lisp. Это очень здорово — возможность пропустить функции, в которых уверен. И еще возможность расставить ловушки и сказать себе: «Сюда мне смотреть не нужно, до тех пор пока этот цикл не повторится семнадцать раз». На PDP-10 были для этого аппаратные средства, это было здорово, особенно в MIT. Тогда они любили модернизировать свои машины, добавляя в них что-нибудь. Можно долго рассказывать про выполнение одного и того же кода разными способами.
Сейбел: Вы применяете к своему коду формальные доказательства?
Стил: Зависит от кода. Если в нем есть сложные математические инварианты, я использую доказательства. Я не стану писать функцию сортировки, пока не подберу какой-нибудь инвариант и не докажу его.
Сейбел: Питер ван дер Линден в своей книге «Expert С Programming» (Программирование на Си для экспертов) отвел доказательствам целую главу в пренебрежительном духе. Вот вам доказательство того-то, но смотрите — оно с ошибками! Ха-ха-ха!
Стил: Да, и доказательства могут быть с ошибками.
Сейбел: Но, по крайней мере, встретить ошибки в них меньше шансов, чем в проверяемом коде?
Стил: Думаю, да, ведь вы используете разные инструменты. Вы используете доказательства затем же, зачем и типы данных, — затем, зачем альпинист пользуется веревкой. Если все хорошо, они не нужны. Но если что-то не так, они увеличивают шанс найти ошибку.
Сейбел: Думаю, худший случай — это ошибка в программе, скрытая ошибкой в доказательстве. Но, к счастью, редкий.
Стил: Такое случается. Не уверен даже, что столь уж редко, ведь вы конструируете доказательства, отражающие структуру кода. И наоборот, если при написании кода вы держите в уме доказательства, это повлияет на структуру вашей программы. Поэтому нельзя говорить о взаимной независимости кода и доказательства в вероятностном смысле. Но можно задействовать разные инструменты, разные способы мышления.
Программируя, вы погружаетесь в разные локальные мелочи, а инварианты дают глобальный взгляд на программу. И доказательства заставляют эти два взгляда взаимодействовать. Вы видите, как локальные шаги воздействуют на глобальный инвариант, который нужно поддержать.
Вот один из самых интересных
Я зарылся в это доказательство и стал проверять его шаг за шагом. Трудность состояла в том, что каждое выражение в программе могло нарушить любой инвариант, поскольку программа была параллельной. Поэтому Овицки предлагала перекрестную проверку в каждой точке. Потратив на это около 25 часов, я обнаружил, что пару шагов я пройти не могу. И сообщил об этом — оказалось, что в этих местах алгоритма были ошибки.
Сейбел: Итак, алгоритм содержал ошибки, и доказательство их пропустило.
Стил: Да, получилось, что доказательство некорректно. Что-то где-то было упущено. Какие-то детали работы с формулой — формула была почти правильна, но именно «почти». Дело было лишь в том, чтобы поменять местами, например, две строки кода.
Сейбел: Итак, 25 часов ушло на то, чтобы проанализировать доказательство. Вы бы смогли найти ошибку в коде за 25 часов, имея перед собой только код и больше ничего?
Стил: Вряд ли бы я даже понял, что там есть ошибка. Алгоритм был довольно мудреным: я посмотрел бы на код, понял его общий смысл — и не заметил бы неточности. Нужна была очень маловероятная последовательность действий, чтобы она проявилась.
Сейбел: И все выявилось в процессе доказательства, то есть вам не надо было рассматривать различные сценарии типа «что, если» для обнаружения проблемы.
Стил: Верно. Доказательства позволяют представить глобальную точку зрения и предусмотреть все возможности, резюмируя их при помощи очень сложной формулы. И чтобы это получить, приходится проработать кучу формул. Автор переработал статью, она снова вернулась ко мне на рецензию — и хотя я уже проделал это упражнение, пришлось опять потратить 25 часов на проверку доказательства. На этот раз, кажется, все было нормально.
Статья вышла, никто больше не находил в этом алгоритме ошибок. Есть ли они там сейчас? Не знаю. Но доказательство дает мне куда больше уверенности в том, что с алгоритмом теперь все нормально. Надеюсь, я не единственный рецензент, разобравшийся в доказательстве.
Сейбел: Дейкстра говорил, что тестирование не позволяет считать программу свободной от ошибок. Вы всего лишь показали, что ваши тесты ошибок не нашли. Но ведь с доказательствами то же самое — вы всего лишь можете сказать, что ваше доказательство не выявило ошибок.