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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Стил:Да. Точно.

Сейбел:О чем еще вы бы хотели поговорить?

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

Есть великолепные алгоритмы, которыми я просто восхищался. Я видел чудесные программы для сжатия кода - в те времена у тебя был всего один мегабайт памяти, и это имело значение. Было важно, сколько слов ты используешь - 40 или 30, и люди временами серьезно работали над тем, чтобы ужать программу. Билл Госпер писал эти шедевры из четырех строк, и они творили потрясающие вещи, например с усилителем, подключенным к младшим битам аккумулятора, который в это время тасовал биты.

Это может показаться бессмысленной тратой сил, но одним из лучших моментов в моей карьере был тот, когда я смог сократить программу Госпера из 11 слов до 10. И это - ценой лишь небольшого увеличения времени выполнения программы, ценой малой доли машинного цикла. Я нашел способ сократить код на одно слово, и на это у меня ушло всего лишь 20 лет.

Сейбел:И вот, спустя 20 лет, вы сказали: “Привет, Билл, а представляешь?..”

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