Грандиозен ли вызов?

После того, как я прослушал на международной конференции «Перспективы систем информатики» в Новосибирске доклад Тони Хоара, а затем познакомился с его интервью («Грандиозный вызов информатике», «Открытые системы», 2003, № 9), у меня возник ряд соображений.

Реализация идеи Верифицирующего Транслятора оценивается Хоаром в тысячу человеко-лет. Несложно оценить, сколько для этого потребуется финансовых средств. Даже взяв на себя смелость установить годовой оклад участника проекта в миллион долларов при норме накладных расходов в 100%, получаем 2 млрд. долл. затрат. Для корпорации Microsoft, которую сегодня представляет Тони Хоар, сумма вполне подъемная. Если выполнять проект в условиях Индии или России, то затраты можно снизить на порядки. Насколько правильно называть это Большим Вызовом? Правомерно ли сравнивать этот проект с полетом человека на Луну, как это недвусмысленно звучит в последних выступлениях Хоара? Почему финансированием этого проекта не занимается сама Microsoft, столь известная своей способностью достигать коммерческого успеха путем реализации своих и чужих идей?

В воздухе повисают и другие вопросы. А что даст Верифицирующий Транслятор? Снимет ли он все проблемы с верификацией программ? Насколько повысит надежность? На каких языках должны быть написаны программы, которые он может верифицировать? Кто и как будет верифицировать сам Верифицирующий Транслятор? Впрочем, на последний вопрос Хоар отвечает, замечая, что Верифицирующий Транслятор не будет верифицирован, что задача его верификации — это отдельный Вызов. Данное замечание по причинам, описанным еще Геделем, рисует перед мысленным взором бесконечную череду Больших Вызовов... Также непонятно, кто будет гарантировать отсутствие ошибок в спецификации, по которой будет проверяться программа? А это весьма серьезная проблема: большое количество неудач при разработке программного обеспечения связано именно с ошибками, возникающими на начальных этапах проектирования при анализе исходных условий и составлении спецификаций.

Некоторые доклады на упомянутой конференции содержали жалобы на то, что в своей массе программисты не проявляют желания использовать уже имеющиеся наработки в области формальной верификации программ. Анализ причин такой грустной ситуации не делается, однако, глядя на доступные иллюстративные материалы, можно сделать вывод о чрезмерном увеличении исходного кода программ за счет верифицирующей надстройки. Код может увеличиться вдвое, а может — и на порядок. Насколько эффективен такой подход с экономической точки зрения?

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

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

Анализируя сложившуюся практику построения программного обеспечения, замечаешь, что для повышения его качества еще имеются значительные резервы. Одним из эффективнейших способов повышения качества программного обеспечения всеми специалистами указывается совершенствование процесса разработки. В первую очередь, за счет внедрения стандартных приемов, уже показавших себя на практике. Как насмешка над этими выводами в отечественном программировании сложилась парадоксальная ситуация. С одной стороны, в России накоплен богатейший практический опыт разработки и сопровождения программного обеспечения, отраженный в Единой Системе Программной Документации (ЕСПД). С другой стороны, на программистских форумах и в научной среде постоянно сталкиваешься с проявлениями невежества. При упоминании ГОСТ или ЕСПД считается нормальным отозваться о стандартах, как об устаревших бюрократизмах, пережитках «эпохи тоталитаризма». Однако хотелось бы заметить, что, к примеру, стандарт ЕСПД на блок-схемы (ГОСТ 19.701-90) полностью соответствует стандарту ISO 5807-85. К слову, этот же стандарт в незначительно модифицированном виде преподносится как откровение в UML, что лишний раз свидетельствует о тотальном разрыве между практикой и наукой, что и отметил Бертран Мейер в интервью в том же выпуске журнала «Открытые системы».

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