Чистая архитектура. Искусство разработки программного обеспечения

В 1955 году, имея трехлетний опыт программирования и все еще будучи студентом, Дейкстра пришел к выводу, что интеллектуальные вызовы программирования намного обширнее интеллектуальных вызовов теоретической физики. В результате в качестве своей дальнейшей стези он выбрал программирование. В 1957 году Дейкстра женился на Марии Дебетс. В то время в Нидерландах требовали от вступающих в брак указывать профессию. Голландские власти не пожелали принять от Дейкстры документы с указанной профессией «программист»; они никогда не слышали о такой профессии. Поэтому ему пришлось переписать документы и указать профессию «физик-теоретик».

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

Свою карьеру Дейкстра начинал в эпоху ламповой электроники, когда компьютеры были огромными, хрупкими, медленными, ненадежными и чрезвычайно ограниченными (по современным меркам). В те годы программы записывались двоичным кодом или на примитивном языке ассемблера. Ввод программ в компьютеры осуществлялся с использованием перфолент или перфокарт. Цикл правка – компиляция – тестирование занимал часы, а порой и дни.

В такой примитивной среде Дейкстра сделал свои величайшие открытия.

Доказательство

С самого начала Дейкстра заметил, что программирование – сложная работа и что программисты справляются с ней не очень успешно. Программа любой сложности содержит слишком много деталей, чтобы человеческий мозг смог справиться с ней без посторонней помощи. Стоит упустить из виду одну маленькую деталь, и программа, которая кажется работающей, может завершаться с ошибкой в самых неожиданных местах.

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

Дейкстра понимал, что для этого он должен продемонстрировать методику написания доказательств на простых алгоритмах. Но эта задача оказалась довольно сложной.

В ходе исследований Дейкстра обнаружил, что в некоторых случаях использование инструкции goto мешает рекурсивному разложению модулей на все меньшие и меньшие единицы и тем самым препятствует применению принципа «разделяй и властвуй», что является необходимым условием для обоснованных доказательств.

Однако в других случаях инструкция goto не вызывала этой проблемы. Дейкстра заметил, что эти случаи «доброкачественного» использования goto соответствуют простым структурам выбора и управления итерациями, таким как if/then/else и do/while. Модули, использующие только такие управляющие структуры, можно было рекурсивно разложить на доказуемые единицы.

Дейкстра знал, что эти управляющие структуры в сочетании с последовательным выполнением занимают особое положение. Они были идентифицированы за два года до этого Бёмом и Якопини, доказавшими, что любую программу можно написать, используя всего три структуры: последовательность, выбор и итерации.

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

Дейкстра показал, что доказать правильность последовательности инструкций можно простым перечислением. Методика заключалась в прослеживании последовательности математическим способом от входа до выхода. Она ничем не отличалась от обычного математического доказательства.

Правильность конструкций выбора Дейкстра доказывал через повторяющееся применение приема перечисления, когда прослеживанию подвергался каждый путь. Если оба пути в конечном итоге давали соответствующие математические результаты, их правильность считалась доказанной.

Итерации – несколько иной случай. Чтобы доказать правильность итерации, Дейкстре пришлось использовать индукцию. Он доказал методом перечисления правильность случая с единственной итерацией. Затем, опять же методом перечисления, доказал, что если случай для N итераций правильный, значит, правильным будет случай для N + 1 итераций. Используя тот же метод перечисления, он доказал правильность критериев начала и окончания итераций.

Такие доказательства были сложными и трудоемкими, но они были доказательствами. С их развитием идея создания евклидовой иерархии теорем выглядела достижимой в реальности.

Объявление вредным