Кодеры за работой. Размышления о ремесле программиста
Шрифт:
Стил: Да, и доказательства могут быть с ошибками.
Сейбел: Но, по крайней мере, встретить ошибки в них меньше шансов, чем в проверяемом коде?
Стил: Думаю, да, ведь вы используете разные инструменты. Вы используете доказательства затем же, зачем и типы данных, - затем, зачем альпинист пользуется веревкой. Если все хорошо, они не нужны. Но если что-то не так, они увеличивают шанс найти ошибку.
Сейбел: Думаю, худший случай - это ошибка в программе, скрытая ошибкой в доказательстве. Но, к счастью, редкий.
Стил:
Программируя, вы погружаетесь в разные локальные мелочи, а инварианты дают глобальный взгляд на программу. И доказательства заставляют эти два взгляда взаимодействовать. Вы видите, как локальные шаги воздействуют на глобальный инвариант, который нужно поддержать.
Вот один из самых интересных случаев в моей практике. Меня попросили написать отзыв на статью Дэвида Гриса для “САСМ”. Грис писал о доказательстве правильности параллельного алгоритма сборки мусора. Сьюзен Овицки была студенткой Гриса и разработала кое-какие инструменты для доказательства корректности параллельных программ. А Грис решил применить их к параллельному сборщику мусора, разработанному Дейкстрой. Код занимал где-то полстраницы. А остальная часть статьи содержала доказательство его корректности.
Я зарылся в это доказательство и стал проверять его шаг за шагом. Трудность состояла в том, что каждое выражение в программе могло нарушить любой инвариант, поскольку программа была параллельной. Поэтому Овицки предлагала перекрестную проверку в каждой точке. Потратив на это около 25 часов, я обнаружил, что пару шагов я пройти не могу. И сообщил об этом - оказалось, что в этих местах алгоритма были ошибки.
Сейбел: Итак, алгоритм содержал ошибки, и доказательство их пропустило.
Стил: Да, получилось, что доказательство некорректно. Что-то где-то было упущено. Какие-то детали работы с формулой - формула была почти правильна, но именно “почти”. Дело было лишь в том, чтобы поменять местами, например, две строки кода.
Сейбел: Итак, 25 часов ушло на то, чтобы проанализировать доказательство. Вы бы смогли найти ошибку в коде за 25 часов, имея перед собой только код и больше ничего?
Стил: Вряд ли бы я даже понял, что там есть ошибка. Алгоритм был довольно мудреным: я посмотрел бы на код, понял его общий смысл - и не заметил бы неточности. Нужна была очень маловероятная последовательность действий, чтобы она проявилась.
Сейбел: И все выявилось в процессе доказательства, то есть вам не надо было рассматривать различные сценарии типа “что, если” для обнаружения проблемы.
Стил: Верно. Доказательства позволяют представить глобальную точку зрения и предусмотреть все возможности, резюмируя их при помощи очень сложной формулы. И чтобы это получить, приходится проработать кучу формул. Автор переработал
статью, она снова вернулась ко мне на рецензию - и хотя я уже проделал это упражнение, пришлось опять потратить 25 часов на проверку доказательства. На этот раз, кажется, все было нормально.Статья вышла, никто больше не находил в этом алгоритме ошибок. Есть ли они там сейчас? Не знаю. Но доказательство дает мне куда больше уверенности в том, что с алгоритмом теперь все нормально. Надеюсь, я не единственный рецензент, разобравшийся в доказательстве.
Сейбел: Дейкстра говорил, что тестирование не позволяет считать программу свободной от ошибок. Вы всего лишь показали, что ваши тесты ошибок не нашли. Но ведь с доказательствами то же самое - вы всего лишь можете сказать, что ваше доказательство не выявило ошибок.
Стил: Это правда. И вот почему есть отрасль компьютерных наук, изучающая автоматическую проверку доказательств. Надежда на то, что программа проверки доказательства окажется корректной. А она будет корректной при небольшом размере. И сделать ее небольшой гораздо проще, чем проверять доказательство какой-либо достаточно большой программы.
Сейбел: И программа автоматической проверки, проверенная вручную, может сэкономить 25 часов, потраченные вами на изучение доказательства фрагмента кода?
Стил: Да. Точно.
Сейбел: О чем еще вы бы хотели поговорить?
Стил: Мы не коснулись такой темы, как красота программ. А мне хочется сказать об этом пару слов. Некоторые программы буквально поражали меня своей красотой. Например, ТеХ, то есть исходный код ТеХ. METAFONT - в меньшей степени, но не знаю, почему: то ли потому, что я работал с ним меньше, то ли потому, что мне и вправду меньше нравятся структура кода и архитектура программы.
Есть великолепные алгоритмы, которыми я просто восхищался. Я видел чудесные программы для сжатия кода - в те времена у тебя был всего один мегабайт памяти, и это имело значение. Было важно, сколько слов ты используешь - 40 или 30, и люди временами серьезно работали над тем, чтобы ужать программу. Билл Госпер писал эти шедевры из четырех строк, и они творили потрясающие вещи, например с усилителем, подключенным к младшим битам аккумулятора, который в это время тасовал биты.
Это может показаться бессмысленной тратой сил, но одним из лучших моментов в моей карьере был тот, когда я смог сократить программу Госпера из 11 слов до 10. И это - ценой лишь небольшого увеличения времени выполнения программы, ценой малой доли машинного цикла. Я нашел способ сократить код на одно слово, и на это у меня ушло всего лишь 20 лет.
Сейбел: И вот, спустя 20 лет, вы сказали: “Привет, Билл, а представляешь?..”
Стил: Ну, собственно, я не занимался этим все 20 лет, просто 20 лет спустя я вернулся к этой программе, и ко мне пришло озарение: я понял, что, изменив один код операции, я получу константу с плавающей запятой, близкую к тому, что мне нужно. И смогу использовать инструкцию и как инструкцию, и как константу с плавающей запятой.
Сейбел: Прямо “История Мэла, настоящего программиста”.