Дейкстра "Дисциплина программирования"

[Olegator]

Здравствуйте.
Кто-нибудь читал эту книгу?
Я начал читать книгу и она мне понравилась.
Он пишет о том, что можно сделать так, чтобы хорошая программа выводилась логически в результате точных критериев, а не только исходя из опыта и туманных соображений.
Хотелось бы знать, действительно ли всё так круто или это только философские размышления и никто из прогаммистов этим не пользуется?

[Alf]

Книга из разряда классики структурного программирования. Бестселлер 70-80 годов.

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

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

Лично мне доводилось доказывать правильность программы считанные разы. Как правило, это связано с работой биллинговых программ, где экспериментальная проверка правильности весьма трудоемка, а цена ошибки весьма высока (программы манипулируют огромными суммами).

[Olegator]

Стоит ли мне её осваивать.

Может быть это позволит упростить со временем написание программ: меньше надо будет заниматься поиском ошибок. Ведь больше времени уходит не на написание программ, а на её отладку.
А так написал сразу хорошо и дальше не мучаешся. Или хотя бы меньше отлаживать?
Хотелось бы знать есть ли продолжение этих его мыслей?
Или может быть другие подобные направления?

[Alf]

Стоит ли мне её осваивать.

Лучше тебя самого на этот вопрос никто ответить не сможет.

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

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

Может быть это позволит упростить со временем написание программ: меньше надо будет заниматься поиском ошибок. Ведь больше времени уходит не на написание программ, а на её отладку.
А так написал сразу хорошо и дальше не мучаешся. Или хотя бы меньше отлаживать?

И не надейся. Царских путей в программировании, равно как и в геометрии, нет и вряд ли когда-либо будут.

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

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

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

Хотелось бы знать есть ли продолжение этих его мыслей?
Или может быть другие подобные направления?

Много лет назад мне попадались очень толковые статьи Вирта на эту тему. Хотел сделать их перевод и опубликовать на нашем сайте, но пока попадались лишь ссылки на коммерческие издания вроде Communications of the ACM, которые хотят денег за скачивание. Если попадутся в открытом доступе, с удовольствием поработал бы над ними. Но пока что кроме Дейкстры, увы, бесплатного ничего не нашел.

[Alf]

Небольшое добавление к сказанному.

Ошибки в программах я бы разделил на две группы:

1. Принципиальные ошибки, связанные с недостаточным пониманием задачи, неверным ее решением и т.п. То есть в основе программы лежит в принципе неверный алгоритм. Для борьбы с такими ошибками и служит доказательство правильности алгоритма/программы.

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

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

[LEON]

Есть одна книга по пректированию программ, она именно для начинающих.
К. Ларман. Применение UML и шаблонов проектирования.
http://www.ozon.ru/context/detail/id/1048352/

Судя по названию в ней должна быть информация по паттернам проектирования, но ее там довольно мало. Зато детально рассматривается процесс создания POS системы, с т.з. современных технологий разработки программ. Вводная информация, о UP унифицированном процессе разработки, о жизненном цикле ПО, об анализе предметной области. Книга дает хорошее представление о том, как разрабатываются программы в настоящее время, но без сильного углубления в детали. в общем для начинающих самое оно.

[Not]

Хотелось бы знать, действительно ли всё так круто или это только философские размышления и никто из прогаммистов этим не пользуется?

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

[Вахмурка]

  Моё мнение: программирование существует и как научная дисциплина и как отрасль промышленности.
Эти вещи между собой пересекаются, но путать их между собой не следует. У меня недавно стояла задача полностью проверить коректность данного алгоритма. Я использовал тестовый прогон со 100% покрытием кода. Доказательство у меня наверно заняло бы больше времени. Хотя существуют алгоритмы тестовый прогон которых возможен только в теории, на практике тут бы потребовалось слишком много времени. Тут если очень надо то надо доказывать.

P.S. А вообше если бы все алгоритмы в программах доказывались, программирование ни когда не стало бы идустрией и многих вещей которыми мы пользуется просто бы не было.

[Not]

У меня недавно стояла задача полностью проверить коректность данного алгоритма. Я использовал тестовый прогон со 100% покрытием кода.

Во-первых стопроцентное покрытие - скорее исключение, чем правило. Во-вторых, неумение увидеть формальную модель часто приводит к концептуальным ошибкам. Которые имеют свойство проявляться за месяц до сдачи проекта. И тут вы хоть десять женщин привлеките, а все равно год будете переделывать, если проблема серьезная. Приведу пример: не так давно некая группа писала транслятор с одного языка на другой. В процессе трансляции предполагалась приведение логических формул в ДНФ. За месяц до завершения проекта ¨выяснилось¨, что алгоритм вообще говоря NP-трудный. И быстро был найден пример задачи, на котором он съедал всю доступную память. Переделка заняла полгода. С выявлением трудных случаев, с преобразованием оных в упрощенный вид и так далее.

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

[Вахмурка]

У меня недавно стояла задача полностью проверить коректность данного алгоритма. Я использовал тестовый прогон со 100% покрытием кода.

Во-первых стопроцентное покрытие - скорее исключение, чем правило.

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

[Dimka]

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

А можно поподробнее раскрыть эту мысль? А то я не вполне понимаю:
1) О какой "формальной структуре" идёт речь? Что это за структура?
2) Почему следование некой структуре спасает от сложности? Всегда?

У меня недавно стояла задача полностью проверить коректность данного алгоритма. Я использовал тестовый прогон со 100% покрытием кода. Доказательство у меня наверно заняло бы больше времени. Хотя существуют алгоритмы тестовый прогон которых возможен только в теории, на практике тут бы потребовалось слишком много времени.

100% покрытия кода тестом - это панацея? Ведь можно написать тест, проверяющий весь код (все участки программы хоть раз выполнятся), но, тем не менее, не проверяющий граничных условий, соответствия вызовов пред- и постусловиям. Разве может одно лишь наличие теста успокаивать, когда мы ничего не знаем о качестве этого теста?

[Вахмурка]

dimka, панацеии нет и никогда не будет. Даже само требование к какому-то модулю может быть не полным и протеворичивым, ошибки могут быть и в доказательствах и в тестовом коде. В моём случае тестовый код проверял правильности выходных данных при изветных входных. Если при 100% покрытии проблем не возникло значит всё ОК. Конечно, другие части программы могут заслать в этот модуль не допустимые данные, на которых его функциональность не определена, но это уже другая история или другой тест.