Эдсгер Вибе Дейкстра. Смиренный гений программирования
www.samag.ru
     
Поиск   
              
 www.samag.ru    Web  0 товаров , сумма 0 руб.
E-mail
Пароль  
 Запомнить меня
Регистрация | Забыли пароль?
Журнал "Системный администратор"
Журнал «БИТ»
Наука и технологии
Подписка
Где купить
Авторам
Рекламодателям
Архив номеров
Контакты
   

  Опросы
  Статьи

Электронный документооборот  

5 способов повысить безопасность электронной подписи

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

 Читать далее...

Рынок труда  

Системные администраторы по-прежнему востребованы и незаменимы

Системные администраторы, практически, есть везде. Порой их не видно и не слышно,

 Читать далее...

Учебные центры  

Карьерные мечты нужно воплощать! А мы поможем

Школа Bell Integrator открывает свои двери для всех, кто хочет освоить перспективную

 Читать далее...

Гость номера  

Дмитрий Галов: «Нельзя сказать, что люди становятся доверчивее, скорее эволюционирует ландшафт киберугроз»

Использование мобильных устройств растет. А вместе с ними быстро растет количество мобильных

 Читать далее...

Прошу слова  

Твердая рука в бархатной перчатке: принципы soft skills

Лауреат Нобелевской премии, специалист по рынку труда, профессор Лондонской школы экономики Кристофер

 Читать далее...

1001 и 1 книга  
19.03.2018г.
Просмотров: 9897
Комментарии: 0
Потоковая обработка данных

 Читать далее...

19.03.2018г.
Просмотров: 8108
Комментарии: 0
Релевантный поиск с использованием Elasticsearch и Solr

 Читать далее...

19.03.2018г.
Просмотров: 8211
Комментарии: 0
Конкурентное программирование на SCALA

 Читать далее...

19.03.2018г.
Просмотров: 5196
Комментарии: 0
Машинное обучение с использованием библиотеки Н2О

 Читать далее...

12.03.2018г.
Просмотров: 5879
Комментарии: 0
Особенности киберпреступлений в России: инструменты нападения и защита информации

 Читать далее...

Друзья сайта  

 Эдсгер Вибе Дейкстра. Смиренный гений программирования

Статьи / Эдсгер Вибе Дейкстра. Смиренный гений программирования

Автор: Алексей Вторников

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

В информатике мы все – дети Дейкстры

К. Апт «Портрет гения»

«Ты помнишь, как все начиналось»

Эдсгер Вибе Дейкстра родился в Роттердаме (Нидерланды) в мае 1930 года в семье научных работников: отец будущего лауреата Тьюринговской премии был химиком, мать – математиком что, видимо, и предопределило выбор Дейкстры поступить на отделение математики и теоретической физики Лейденского университета. Еще учась в университете Дейкстра познакомился с первыми компьютерами и увлекся их программированием. Этому немало способствовало и то, что будучи еще студентом Дейкстра с 1952 года работал программистом в Математическом центре Амстердама. За год до окончания университета Дейкстра оказался перед дилеммой: продолжить научную карьеру по основной специальности – теоретической физике или все-таки продолжать заниматься программированием. Вот что рассказывал об этом он сам: 

Эдсгер Вибе Дейкстра
Эдгер В. Дейкстра:
«Если отладка – процесс удаления ошибок, то программирование должно быть процессом их внесения»

«... мне надо было сделать выбор – либо прекратить программировать и стать настоящим респектабельным теоретическим физиком, либо как-то формально завершить мое обучение теоретической физике с минимальными усилиями и стать ... кем же? Программистом? Но разве это респектабельная профессия? В конце-концов, что такое программирование? В чем должен был состоять тот солидный объем знаний, который позволил бы считать программирование научной дисциплиной?»

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

Трудно сказать – много ли потеряла теоретическая физика оставшись без Дейкстры; учитывая его уникальную интеллектуальную мощь, которая очень вскоре проявилась в полную силу, рискну предположить, что физика потеряла немало. Но случилось то, что случилось и начиная с этого времени талант и энергия Э.Дейкстры принадлежали новой дисциплине – информатике.

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

Однако, ближайшие несколько лет показали – ван Вейнгаарден не ошибся, предложив своему талантливому студенту, а в дальнейшем аспиранту, выбрать программирование: с конца 50-х годов корпорация IBM начала производство компьютеров на транзисторах, что позволило существенно снизить их энергоемкость, массу и стоимость одновременно подняв объемы памяти и производительность. Моментально подтянулись другие компании и компьютеры из военных и научных лабораторий стали доступны банкам, производственным предприятиям, учебным заведениям, больницам, коммунальным службам... Компьютерная эра началась.

В обычной жизни Э.В.Дейкстра был по-хорошему «чудаковат»: предпочитал простую ручку компьютеру, в его доме не было телевизора, он не пользовался мобильным телефоном, не смотрел кино. Когда его коллеги подготовили и издали к 60-летнему юбилею специальный сборник, Дейкстра ответил каждому из них личным благодарственным письмом, написанным от руки (а это, между прочим – 61 адресат). Ученому его уровня и положения полагался секретарь, но Дейкстра отказался от этой привилегии и все предпочитал делать сам. Любил музыку и был хорошим пианистом. В августе 2002 года Эдсгер Вибе Дейкстра скончался в своем доме в Нидерландах.

Рассказать обо всем, что сделал Эдсгер В.Дейкстра в рамках небольшой журнальной статьи невозможно – этому можно посвятить книгу и, наверное, не одну; лучше всего – обратиться непосредственно к каталогу его работ, благо он находится в свободном доступе. Я расскажу лишь об основных работах Дейкстры, в которых, на мой взгляд, наиболее ярко раскрылся его талант исследователя, интуиция философа, незаурядный дар писателя и исключительная скромность, присущая истинно великим (кстати, слово «смиренный», использованное мною в названии статьи, взято из Тьюринговской лекции «Смиренный программист», прочитанной Дейкстрой в 1972г.).

Алгоритм кратчайшего пути на графе

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

Алгоритм Дейкстры широко применяется и сегодня (например, при планировании автомобильных и авиа-маршрутов, при разводке электронных плат, в протоколах маршрутизации). Относится к «жадным» алгоритмам, т.е. достаточно эффективен для поиска путей на относительно небольших графах. Он описан во множестве книг и статей по структурам данных к которым я и отсылаю заинтересованного читателя. Там же можно найти анализ алгоритма Дейкстры и примеры его реализации.

ALGOL-60

Порядком намаявшись в начале своей программистской карьеры с машинными кодами и с тем, что для различных моделей компьютеров один и тот же алгоритм нужно было переписывать практически с нуля, Эдсгер Дейкстра не мог не «ухватиться» за языки программирования высокого уровня. FORTRAN, появившийся в конце 50-х годов Дейкстру не очень привлекал: в FOTRAN-е многое было принесено в жертву главной цели - во чтобы то ни стало реализовать высокоуровневый язык и избавить программиста от «проклятья» двоичных кодов. Появись FORTRAN сегодня, его шансы удержаться, думаю, были бы весьма сомнительными. Но тогда, безусловно, FORTRAN был великим шагом вперед. Однако, Дейкстре все равно FORTRAN не импонировал – ему в этом языке, по-видимому, не хватало того изящества и логичности конструкций, которые Дейкстра привык видеть в математике и логике.

Другое дело ALGOL-60. Язык описывался стройной и вполне строгой нотацией (т.н. называемая «форма Бэкуса-Наура»), его разработка велась едва ли не в академической среде с присущими последней требованиями четкости, ясности и доказуемости. Критерии были строгими и язык поэтому получился изящный (не случайно такие языки программирования как PL/1, PASCAL и ADA носят явные следы влияния ALGOL-а). Не мешкая Дейкстра приступил к реализации компилятора и успех в этом направлении подтвердил его давнюю мысль – программировать надо на «нормальных» языках, приспособленных, насколько это возможно, к психологии человека. А машинный код – ну что же, раз без него все равно никуда не деться – его можно и нужно оставить машинам.

Одной из наиболее сложных задач при трансляции языков программирования в те годы была задача компиляции арифметических выражений с учетом приоритетов операций и скобок. Дейкстра убедительно обосновал и упростил предложенный в 1957г. Ф.Брауэром и К.Замельзоном алгоритм использования для этой цели двух стеков (тогда обычно говорили «магазин» по аналогии с магазином оружия). Арифметические выражения эффективно транслировались в обратную (или «инверсную») польскую запись очень удобную для генерации объектного кода.

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

Борьба за ресурсы или взаимодействие процессов

Разработчики первых операционных систем, которые и операционными системами можно назвать с большой натяжкой, работавших в пакетном режиме (когда одному заданию полностью «принадлежали» все ресурсы компьютера) почти не сталкивались с задачей, которая к середине 60-х годов прошлого века стала чрезвычайно актуальной – обеспечение доступа нескольких процессов к общим ресурсам и разделение этих ресурсов между процессами. Без этого нельзя было решить важнейшую задачу – одновременное выполнение нескольких процессов на одном компьютере.

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

Наиболее полно свои мысли по этому поводу Дейкстра изложил в статье «Взаимодействие последовательных процессов». Для решения этой проблемы Дейкстра предложил концепцию «семафора» - специальных целочисленных общих переменных и  двух примитивов «P-операция» и «V-операция». Вот как сам Дейкстра описывает эти примитивы:

«Эти две последнии операции всегда выполняются над семафорами и представляют единственный способ обращения к семафорам со стороны одновременно действующих процессов.

Семафоры являются по существу неотрицательными целыми величинами. Если они используются только для решения задачи взаимного исключения, то область их значений составляют лишь «0» и «1».»

V-операция состоит в увеличении значения аргумента (который является семафором) на 1. Такое увеличение обязано быть неделимой операцией. P-операция, напротив, будучи применной к семафору, уменьшает (также неделимым образом) значение последнего на 1. Поскольку семафор, согласно определению, число неотрицательное, то рано или поздно P-операция уменьшит его значение до 0. Процесс, инициировавший P-операцию вынужден будет ждать (т.е. фактически окажется в режиме задержки выполнения) до тех пор пока другой процесс не «сдвинет» значение этого семафора в положительную область, т.е. разблокирует семафор.

Эти концепции и их дальнейшее развитие – например, мьютексы – и сегодня применяются при проектировании и реализации операционных систем.

В эти же годы Эдсгер Дейкстра руководил созданием операционной системы THE (от «Technische Hogeschool Eindhoven») с поддержкой многозадачности. Операционная система была построена в виде иерархии из 6 уровней; при этом более низкие уровни (начиная с 0) служили базой для более высоких (вплоть до 5). На начальных уровнях были реализованы система обработки прерываний, семафоры, переключение контекстов процессов, система управления памятью, диспетчер. На средних уровнях были реализованы взаимодействие с консолью, ввод/вывод, взаимодействие с устройствами; самый верхний уровень предназначался для пользовательских программ. В дальнейшем такая модель организации операционной системы получила широкое распространение.

Для иллюстрации проблемы разделения/блокирования ресурсов и взаимодействия процессов Дейкстра предложил простую и остроумную модель; позже эта модель получила имя «задачи о пяти обедающих философах». Вот она в изложении Ч.Хоара (с ним мы еще встретимся):

«В давние времена один богатый филантроп пожервовал свой капитал на основание некоего пансиона, чтобы дать пристанище пяти знаменитым философам. У каждого философа была своя комната, где он мог предаваться размышлениям. Была у них и общая столовая с круглым столом, вокруг которого стояли пять стульев, каждый помеченный именем того философа, которому он предназначался... Слева от каждого философа лежала золотая вилка, а в центре стояла большая миска спагетти, содержимое которой постоянно пополнялось.

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

Видит ли читатель в чем тут проблема?

Структурное программирование

Начну с цитаты Эдсгера Дейкстры из его знаменитой статьи «Заметки по структурному программированию»:

«Речь идет о построении больших программ, запись которых может оказаться, скажем, такого же размера, как весь текст этого раздела... Было бы прекрасно, если бы мне удалось проиллюстрировать различные методы на примерах малых программ, а затем закончить фразой: «... и столкнувшись с программой, в тысячу раз большей, вы построите ее точно таким же способом». Однако ... один из тезисов моей работы в том и состоит, что любые два объекта, которые отличаются в чем-то по меньшей мере в сто или более раз, становятся совершенно несопоставимыми.»

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

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

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

«Я считаю, что программа никогда не является самоцелью; программа предназнается для того, чтобы вызвать вычисления, а цель вычислений – получить нужный результат... Я утверждаю (хотя и не могу доказать), что легкость и гибкость таких наших суждений существенно зависит от простоты взаимосвязей между программой и вычислениями... Грубо говоря, можно считать желательным, чтобы структура программы отражалась в структуре вычислений.»

Для обеспечения указанных легкости и гибкости Дейкстра предлагает проектировать и кодировать программы в соответствии с определенной дисциплиной, названной им структурным программированием. Известно (это математический факт известный как теорема Бема-Якопини), что любую программу можно построить с использованием трех конструкций: последовательного выполнения и операторов выбора и цикла. Дейкстра предложил (одновременно, хотя и независимо с Никлаусом Виртом – еще одним лауреатом премии Тьюринга) представлять программу как иерархическую структуру блоков, каждый из которых выполняет небольшую, но завершенную задачу. Это достигается с помощью механизма процедур и функций.  Т.о. программы приобретали модульность.

Идеи структурного программирования, поначалу встреченные с недоверием, довольно скоро завоевали признание (особенно, после создания Никлаусом Виртом языка программирования PASCAL). Более того, эта методика остается актуальной и сегодня (достаточно вспомнить такие популярные языки программирования C, PASCAL или BASIC).

Заканчивая этот раздел, я не могу не удержаться, чтобы не процитировать самое, пожалуй, знаменитое высказывание Эдсгера Дейкстры: «Тестирование программ может служить для доказательства наличия ошибок, но никогда не докажет их отсутствия». И тут самое время перейти к главному труду Эдсгера Дейкстры – его книге «Дисциплина программирования».

Книга

Если бы в русском языке существовала категория артиклей, то я непременно поставил перед названием этого раздела определенный артикль (ср. англ. «The Book»), чтобы подчеркнуть уникальное значение книги Э.Дейкстры «Дисциплина программирования». Книга появилась в 1976 году и через два года была переведена и опубликована на русском языке в серии «Математическое обеспечение ЭВМ». Аналогов «Дисциплине программирования» нет – эта книга уникальна как по замыслу, так и по стилю. «Дисциплина программирования» относится к тем немногим (исчисляющимся двумя-тремя десятками) книгам, определившим столбовые направления и продолжающим оказывать влияние на информатику.

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

В известном смысле «Дисциплина программирования» - это продолжение исследований Э.Дейкстры по структурному программированию, построению алгоритмов и развитию методов программирования. Книге, как и другим работам Дейкстры, присущ тонкий юмор, глубина проникновения в проблемы и искусство воплощения идей в алгоритмы и программы. Дейкстра как бы говорит: «Посмотрите, как можно рассуждать о программах, как можно их проектировать так, чтобы на любом этапе разработки вы не теряли уверенности в правильности – логической, семантической, математической – того, что вы делаете».

Формально книга представляет собой описание решений примерно двух десятков задач, начиная от самых простых (алгоритм Евклида нахождения наибольшего общего делителя), до весьма сложных (построение выпуклой оболочки по заданным точкам в 3-х мерном пространстве). Если бы книга ограничивалась только этим, то, безусловно, она была бы интересна, познавательна, но не более.

Для Дейкстры решенные в книге задачи не самоцель, а способ продемонстрировать способы рассуждения о программах при их построении. Программа, по замыслу автора, должна строиться параллельно с доказательством ее правильности. Вспомните его слова о тестировании. И, конечно, Дейкстра не против отладки – все мы, в конце-концов, люди и всем нам свойственно ошибаться. Дейкстра против того, чтобы отладка была последним (или, хуже того – единственным) критерием проверки правильности и полноты программы. Когда доказательства правильности и полноты строятся вместе с написанием самой программы, то наша уверенность в том, что достигнутый результат отвечает всем этим критериям и наша уверенность в том, что в программе нет ошибок резко (в идеале – до 100%) возрастает. Программирование – не набор пассов и заклинаний, не шаманство, не танцы с бубном, а математическая дисциплина. А всякая дисциплина, если она претендует на нечто большее, чем на внешний эффект, должна строиться на прочном фундаменте. Таким фундаментом для Дейкстры является математическая логика, а точнее – исчисление предикатов. Сейчас это не кажется чем-то необычным, но в те годы это прозвучало как откровение. Дейкстра понял и убедительно показал, как теория может и должна помочь практике.

В конце 60-х годов XX века американцем Р.Флойдом и англичанином Ч.Хоаром - оба, кстати, Тьюринговские лауреаты - было начато исследование формальных свойств программ. Нельзя сказать, что до них этими вопросами никто не занимался, но предыдущие исследования (за исключением, пожалуй, передовых статей создателя языка LISP Дж.Мак-Карти) носили довольно фрагментарный характер. Самые проницательные исследователи понимали, что назревал кризис, обусловленный сложностью и объемом программного обеспечения: индустрии грозила опасность захлебнуться в миллионах строк кода. Ч.Хоар, используя идеи Р.Флойда, предложил формализм для обозначения частичной корректности программ. Этот формализм выражался формулой вида:

{Q} S {R}

имевший следующий смысл: если команда S начинается в начальном состоянии, удовлетворяющем предикату (т.е. условию) Q, то имеется гарантия , что выполнение S заканчивается через конечное время в состояниии удовлетворяющему предикату (т.е. условию) R.

Это все, конечно, очень и очень абстрактно; сейчас я, в качестве примера, рассмотрю реализацию на языке программирования Java алгоритма определения наибольшего общего делителя (НОД) пары целых чисел по алгоритму Евклида:

Void gcd (int x, int y) {

     while (x != y) {

         if (x > y) x = x – y;

         if (x < y) y = y – x;

     }

     System.out.println (x);

}

Теперь проверим как работает эта реализация при различных значениях аргументов:

X y gcd (x, y)
111 259 37
259 111 37
111 257 1
0 257 Бесконечный цикл
0 0 Не определено
-111 259 Ошибка
-111 -259 Ошибка

Вызов gcd (0, 257), очевидно, работает не так как надо: правильный результат 257. Для пары (0, 0) результат вообще не определен: любое число исключая 0 служит решением. Последние два варианта (когда один или оба аргумента метода отрицательны) не позволяют определить правильный результат (он, кстати, равен по-прежнему 37). Одним словом – либо неполна реализация (в ней не обрабатываются особые случаи), либо я передаю недопустимые значения входных аргументов.

Кто в этом виноват? Конечно, программист – он обязан был это предусмотреть какие значения аргументов допустимы, а какие нет. Причем еще на этапе написания программы. Можно ли предотвратить подобные ситуации? Можно. Как именно? Ответ и его обоснование и находятся в книге Дейкстры.

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

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

Вот что пишет Дейкстра:

«Условие, характеризующее множество всех начальных состояний, при которых запуск обязательно приведет к событию правильного завершения, причем система останется в конечном состоянии, удовлетворяющем заданному постусловию, называется «слабейшим предусловием, соответствующим этому постусловию». (Мы называем его «слабейшим», поскольку, чем слабее условие, тем больше состояний удовлетворяют ему, а мы стремимся здесь охарактеризовать все возможные начальные состояния, которые неизбежно приведут к желаемому конечному состоянию.)

Если система (машина, конструкция) обозначается через S, а желаемое постусловие - через R, то соответствующее слабейшее предусловие мы обозначим wp (S, R)»

(здесь «wp» – это аббревиатура от «weakest precondition»).

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

Таким образом методика построения программ по Дейкстре носит характер поиска начальных условий при которых программа S будет правильно завершена (т.е. окажется в состоянии, удовлетворяющем R). Очень важно сделать такой поиск систематическим; поиск вслепую, как это продемонстрировано выше, не подходит. Для этого Дейкстра привлекает аппарат исчисления предикатов из математической логики; начальные условия не просто ищутся - они выводятся: убедительны не голословные утверждения и не результаты тестовых прогонов, а исключительно математически доказуемые факты. При этом доказательство программы строится параллельно ее написанию. Выгоды этого очевидны – мы получаем более или менее убедительные (в зависимости от глубины анализа) свидетельства того, что программа делает то, что от нее ожидается.

Этот подход – вдохновленный работами Р.Флойда и Ч.Хоара и убедительно развитый Эдсгером Дейкстрой – получил имя «формальной верфикации» программ. Для демонстрации разработки программ посредством логического вывода Дейкстра в своей книге описывает очень простой язык программирования, напоминающий в своих основных чертах ALGOL-60, язык настолько простой, что в нем даже нет процедур. В обоснование синтаксиса и семантики этого языка, Дейкстра, следуя своей же методике, дает строгие доказательства поведения основных конструкций – прежде всего, оператора выбора и оператора цикла. Для этого он вводит понятие охраняемых команд, выполнение которых зависит от состояния т.н. предохранителей. Одним словом, Дейкстра стремится обеспечить полную уверенность в том, что его инструментарий свободен от подводных камней и неожиданных особенностей.

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

«Разница между «старой программой» и «новой программой» столь же глубока, сколь глубока разница между гипотезой и доказанной теоремой или между математическим наблюдением и утверждением, строго выведенным из свода постулатов...

Новые формализмы всегда страшат, и требуются значительные и тщательные педагогические усилия, чтобы убедить новичка в том, что формализм не только полезен, но и необходим»

Мне кажется, основной причиной того, что методика Э.Дейкстры так и не стала mainstream-ом заключалась в определенных требованиях к математической культуре программистов (хотя ничего сверх самого элементарного курса математической логики и скромных способностей к абстрактному мышлению не требуется). Кроме того, радикальное снижение стоимости программного обеспечения и стремительное проникновение компьютеров во все области науки, производства и быта требовало все большего объема программного обеспечения и увеличения скорости его разработки. Стоимость труда программиста стала определяющим экономическим фактором. Но за все надо платить. Если цена ошибки программного обеспечения космической ракеты или медицинского томографа очень высока и тут необходимо обеспечить более строгий подход (хотя именно эти области как раз и «отличились» катастрофическими ошибками), то ошибка в игровой программе, броузере или редакторе текста стали зачастую восприниматься как «недокументированная возможность».

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

Было бы глупо и смешно пересказывать «Дисциплину программирования» - ее надо прочесть. То, о чем я рассказал – лишь малая часть того интеллектуального богатства щедро рассыпанного автором на страницах его книги.

Афоризмы

На этом мой небольшой рассказ об Эдсгере В.Дейкстре подошел к концу. Но рассказ о нем будет не полон без упоминания о еще одной стороне творчества великого программиста – его афоризмах, ставших поистине «народным» программистским фольклором. Некоторые из них весьма резки, например: «Студентов, ранее изучавших Бейсик, практически невозможно обучить хорошему программированию. Как потенциальные программисты они подверглись необратимой умственной деградации». Другие более сдержанны: «Средства не виноваты в том, что их безграмотно используют» или «Если отладка - процесс удаления ошибок, то программирование должно быть процессом их внесения». Сами афоризмы отнюдь не тщеславное желание их автора прослыть остроумным человеком; они - концентрированное выражение опыта, интуиции и тонкого аналитического мастерства Эдсгера Вибе Дейкстры – смиренного гения программирования.

Список литературы

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

E.W.Dijkstra Archive http://www.cs.utexas.edu/users/EWD/

Электронный архив трудов и рукописей Эдсгера В.Дейкстры

Э.Дейкстра «Взаимодействие последовательных процессов» (сборник статей «Языки программирования») – М.:, Мир, 1972

Э.Дейкстра «Заметки по структурному программированию» (сборник статей «Структурное программирование») – М.: Мир, 1975

Э.Дейкстра «Дисциплина программирования» - М.: Мир, 1978

Д.Грис «Наука программирования» - М.: Мир, 1984

Адаптированный вариант «Дисциплины программирования», написанный как учебник программирования для университетов. Изложение весьма строгое, но доступное (вся необходимая математика излагается в книге). По словам редактора книги академика А.П.Ершова «... книга Д.Гриса – апостольское деяние, направленное на то, чтобы превратить учение одиночки в мировую религию»

С.Алагич и М.Арбиб «Проектирование корректных структурированных программ» - М.: Радио и Связь, 1984

Более простая книга, нежели работа Д.Гриса. Математики заметно меньше, зато много практических примеров и упражнений. Основной язык программирования - PASCAL

Ч.Хоар «Взаимодействующие последовательные процессы» - М.: Мир, 1989

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

C.A.R.Hoare «An axiomatic basis of computer programming». Communications ACM, v.2 (October 1969), p.576-580, 583

Пионерская работа Ч.Хоара о построении формального базиса программирования

В.Аджиев «Мифы о безопасном ПО: уроки знаменитых катастроф» – журнал «Открытые Системы», июнь 1998 (http://www.osp.ru/os/1998/06/179592/)

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

Комментарии отсутствуют

               Copyright © Системный администратор

Яндекс.Метрика
Tel.: (499) 277-12-41
Fax: (499) 277-12-45
E-mail: sa@samag.ru