Как следствие, весьма актуальны сегодня вопросы качества программного обеспечения и создания средств, способных свести к минимуму число ошибок, в частности, путем четкой верификации формальных спецификаций и создания надежных программных компонентов. Признанные гуру Энтони Хоар (Tony Hoare) и Бертран Мейер (Bertrand Meyer) знакомят читателей журнала «Открытые системы» со своими взглядами на проблему повышения надежности программ. Оба известных специалиста приняли участие в работе международной конференции «Перспективы систем информатики», прошедшей летом этого года в Новосибирске, и ответили на вопросы журнала.

Верифицирующий компилятор — путь к надежным программам

Многие ошибки в программном обеспечении являются следствием несовершенства процедуры взаимодействия человека и компьютера. Однако человек продолжает вмешиваться в цепочку управления, считая, что он более адекватно, чем компьютерная программа реагирует на изменение ситуации. Если добиться от программы более высокой надежности, то, может быть, удастся свести к минимуму влияние человеческого фактора и одним из инструментов повышения качества программ, бросающим грандиозный вызов информатике, может стать верифицирующий компилятор (VC, Verifying Compiler), идею возрождения работ над которым сегодня продвигает Тони Хоар.

«Коммерческое программное обеспечение всегда будет содержать ошибки и только силами независимых общественных организаций, объединяющих академические, государственные и промышленные структуры, можно сделать великий вызов ИТ-индустрии», — Тони Хоар

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

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

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

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

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

Имеется еще масса факторов, позволяющих говорить об актуальности проблемы создания VC, подробное обсуждение каждого из которых потребует отдельной статьи: опыт по созданию спецификаций отказоустойчивых конфигураций; успехи теории программирования, в частности, в области доказательства корректности объектно-ориентированных программ; востребованность рынком оптимизирующих компиляторов.

Как надо подходить к решению такого рода задач?

Ясно, что одной команде не по силам создание VC. Проект VC требует консолидации усилий исследователей из всех развитых стран Старого и Нового Света. Сама идея проверки корректности процедур была высказана еще Аланом Тьюрингом в 1949 году (A. M. Turing, Checking a large routine. Report on a Conference on High Speed Automatic Calculating Machines. Cambridge University, Math. Labs, 1949). Затем, в 1963 году она была развита предложением использовать для этой цели компьютеры (J. McСarthy, Towards a mathematical theory of computation. Procs. of IFIP Congress, 1963, North-Holland, Amsterdam), а в 1967 году переросла в идею компилятора (R.W. Floyd, Assigning meanings to programs. Procs. Of American Society of Applied Mathematics Symposium, 1967). Однако все ранние попытки конкретной реализации наталкивались на противодействие со стороны коммерческих компаний и наличие «зоопарка» аппаратных платформ.

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

И поверьте, бороться есть за что. Например, по данным Министерства торговли только в США общая стоимость используемых сегодня ненадежных программ составляет 60 млрд. долл. Вполне естественно, что не дожидаясь результатов проекта по VC многие компании, в том числе и Microsoft, предлагают сегодня стратегии создания «заслуживающего доверия» программного обеспечения (trustworthy software). Первым промежуточным результатом использования VC может быть формирование условий, при которых хотя бы с вероятностью 80% коммерческие программные продукты первые 10 лет своей эксплуатации не будут требовать выпуска заплаток.

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

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

Можно ли теоретически доказать корректность хотя бы программ на языке Си++?

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

Принимали ли вы участие в создании этой программы?

Да, но только как консультант и частично как архитектор. Я принимал участие в обсуждении концепции, разрабатывая теоретические основы продуктов такого рода. Данная программа анализирует код на языках Cи/Cи++, проверяет дефекты идентификации, корректность типов переменных, правильность выполнения вызовов функций и т.п. Исходный код поступает на синтаксический анализатор Си/Си++, затем обрабатывается «моделером» — самой главной и сложной частью PREfix, который изучает порядок выполнения конструкций языка, сравнивает код с модельными конструкциями и формирует записи для базы ошибок. Затем через Web-интерфейс на экран выдается текст исходного кода с замечаниями о корректности применения той или иной конструкции и описанием последствий их использования. На сегодняшний день программы такого рода представляют собой аккумулятор опыта, собранного в базе данных, однако, как известно, существует большая разница между теорией и практической реализацией и PREfix можно считать еще только одним шагом на пути к VC.

Но в мире используют не только Си или Си++. Имеется еще много языков, каждый из которых занимает свою нишу и играет собственную роль. Какие-то языки формулируют абстракции конкретной прикладной области; другие представляют собой отличный научный инструментарий; третьи аккумулируют опыт. Языки живут, получают расширения, и я не думаю, что когда-либо появится некий универсальный язык, способный решить все проблемы какой-либо отрасли приложений. Со своей стороны, VC должен уметь работать со всеми языками.

In object we trust

На пути преодоления извечных проблем, преследующих проекты создания программного обеспечения (рамки бюджета, баланс сложности, возможность расширения, сроки и проч.) разработчики нередко теряют контроль над качеством программ. На рынке сегодня обращается масса программ, полностью доверять которым нельзя: скрытые в них ошибки могут проявиться в самый неожиданный и ответственный момент. Идея, которую предлагает профессор Бертран Мейер, не нова, однако сегодня она получает совершенно новое звучание — программирование с использованием так называемых «заслуживающих доверия компонентов» (trusted component).

«Одним из следствий увеличивающегося разрыва между наукой и практикой является сегодня то, что промышленность очень мало интересуется качеством программного обеспечения, почти не используя уже имеющиеся формальные методы и инструменты, разработанные в академической среде», — Бертран Мейер

Какие из тенденций, наблюдающихся сегодня в программной инженерии, вы бы выделили?

Прежде всего, хочу отметить, что сегодня в индустрии программирования очень мало плодотворных идей, хотя общую обстановку, которая сложилась, например, с качеством программ трудно назвать благополучной. На мой взгляд, сегодня стоит обратить внимание на два момента: компоненты и формальные методы. Вместо того чтобы плодить все новые модули, можно использовать уже имеющиеся компоненты. Мы называем это программированием в стиле Google-and-Paste («нашел и используй»). Однако грош цена программе, если в ней есть хотя бы один компонент, содержащий ошибку — это как раз и есть сегодня узкое место в программной инженерии.

Формальные методы сегодня уже не интересны ИТ-сообществу. Мало кто думает, что такие методы могут помочь в реальной работе, хотя сегодня они стали гораздо более практическими, чем десять лет назад. Четкие спецификации и унифицированные инструменты создания программного обеспечения позволят создавать надежные компоненты. Чтобы теоретически доказать, например, качество программы на языке С++, нужно, чтобы эта программа изначально была написана в стиле, допускающем возможность проведения такого доказательства, а без знания ряда формальных методов сделать это затруднительно.

Над чем вы сейчас работаете?

Самая важная тема моих исследований — многократно используемые компоненты гарантированного качества. Отрасль еще не думает в достаточной мере о качестве программного обеспечения (возможно, время еще не пришло), но, учитывая, продолжительность жизненного цикла многих программ, предпринимать адекватные усилия надо уже сейчас. Другое направление работ — объектно-ориентированные технологии, развитие языка Eiffel, его новых концепций и конструкций. Очень серьезные работы по улучшению идут в рамках деятельности по подготовке этого языка к стандартизации.

Складывается впечатление, что Eiffel не получил того распространения, которое заслуживал. Почему, особенно если учесть, что в нем имеются сильные средства разработки надежного программного обеспечения?

Прежде всего, Eiffel — это не язык программирования, как считают многие, а метод, помогающий мыслить по-иному при проектировании и создании программ. Метод, способствующий практически полному исключению внесения ошибок в код. В то же время, что до сих за Eiffel не стоял ни один крупный игрок ИТ-рынка, как это было, например, со Smalltalk, который был разработан в корпорации Xerox, хотя мы и пытались предложить этот проект ведущим производителям. Позволяя быстрее и почти без ошибок разрабатывать программы, Eiffel отбирает работу у экспертов и консультантов. Этот инструмент им не интересен, они его не продвигают, а к их мнению прислушиваются поставщики программного обеспечения — не всем еще выгодно создавать изначально более надежные, чем в среднем по отрасли, программы. Хотя я не совсем согласен, что Eiffel исключительно академическая разработка: его сегодня используют такие компании, как EMC, Hewlett-Packard, Computer Associates и CAP Gemini.

Как вам удается совмещать академическую работу с работой в коммерческих компаниях?

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

Бытует мнение, что наука и практика все более удаляются друг от друга?

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

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

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

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

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

По моему мнению, в основе образовательных курсов должны быть языки Паскаль, Модула-2 и Оберон. Надо также знать Cи, Cи++, Java/C#, Perl, Пролог и JavaScript, но специальных курсов по конкретному языку быть не должно. Если вы знаете английский, то сможете самостоятельно прочитать Шекспира или Бернса, а специальное изучение этих произведений даст мало толку. В конечном итоге, студенты должны понимать, что такое программная инженерия, профессионально владеть основными методами, чтобы быстро адаптироваться к конкретным требованиям работодателя.

Еще совсем недавно считалось, что объектно-ориентированное программирование будет доминировать и вытеснит структурное. Оправдались ли такие ожидания?

Структурное и объектно-ориентированное программирование соотносятся как классическая и релятивистская механика — одна является частью другой и каждая работает в своем измерении. В разных условиях удобнее использовать какую-то одну, но никто еще не нашел ничего лучше, чем объектно-ориентированное программирование. Здесь, кстати, уместно вспомнить первоисточники — известную книгу «Структурное программирование». Цитируя ее, обычно упоминают только первые две главы: «Заметки по структурному программированию» Дейкстры и «О структурной организации данных» Хоара. Однако там была еще и третья глава, которую написал У. Дал, и она уже тогда была посвящена объектно-ориентированным технологиям, языку Симула-67. Но так как это была последняя глава, ее обычно никто внимательно не читал, и она тогда осталась почти незамеченной.

Как вы относитесь к UML?

Мне непонятно, почему ИТ-отрасль так увлеклась UML, и зачем корпорации IBM нужно было покупать Rational. Неясно, какую пользу может принести UML технологиям программирования: от модели UML до реального программирования дистанция огромного размера.

Появление .Net вызвало оживление в среде разработчиков языков программирования; вы также поддерживаете эту технологию. В чем перспективы .Net?

Безусловно, .Net — это больше чем просто маркетинговый шум, однако, на сегодняшний день перспективы этой технологии еще неясны. Например, Java появилась относительно недавно, но уже завоевала популярность; потеснить эту технологию на рынке будет весьма непросто. У нас сложились неплохие, хотя и непростые отношения с Microsoft. Относительно .Net удивляет другое — почему компания много говорит про технологии Web-служб, однако почти ничего о более насущных вещах, а именно, о среде разработки для .Net. Для разработчиков наиболее интересна многоязыковая природа .Net. В этой связи Microsoft очень опасно слишком много рекламировать преимущества и перспективы только одного языка. Поэтому мне очень странно наблюдать пропаганду компании, направленную в этом направлении. В мире всегда будет место для многих культур, как, например, в Швейцарии, где мирно сосуществуют три языка. Кроме этого, очень жаль, что Microsoft не передает ИТ-сообществу продукт PREfix. Для индустрии в целом это было бы весьма полезно. Однако, инструменты такого класса — это постфактум, попытка улучшить уже созданный код, меня же больше интересует априорный подход по созданию программного обеспечения, изначально не содержащего — или почти не содержащего — ошибок.

А если завтра Microsoft предложит вам работу, вы, как Хоар, примете это предложение?

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

Профессор сэр Энтони Хоар получил весьма разнообразное образование: изучал греко-латинскую философию, математическую логику, а в годы службы в ВМФ Великобритании осваивал русский язык. Пройдя курсы программирования, в 1959 году он учился в МГУ под руководством А.Н. Колмогорова на курсе трансляции алгоритмических языков. Здесь же предложил один из известных алгоритмов сортировки. Вернувшись в Англию в 1960 году, работал программистом в компании Elliott Brothers, поставлявшей компьютеры для научных исследований, затем трудился в команде, создавшей первый коммерческий компилятор для Algol 60. Принимал участие в проектах по созданию первых операционных систем, был архитектором программного обеспечения и аппаратного обеспечения ряда компьютеров того времени. В 1968 году начал заниматься научной деятельностью в Королевском университете Белфаста, поставив перед собой задачу разобраться, почему операционные системы столь сложны по сравнению с компиляторами и как теория программирования и языки могут решить задачу распараллеливания. В 1977 году Хоар перешел в Оксфордский университет и создал исследовательскую группу Programming Research Group, в задачу которой входит укрепление связей промышленных, академических и государственных структур, работающих в области ИТ-индустрии. Тематика его исследований в Оксфорде: корректность программных спецификаций, проектирование и разработка критичных и некритичных систем.

Наиболее известные результаты его работы: язык Z спецификаций и параллельная модель взаимодействия последовательных процессов (CSP, Communicating Sequential Process). В числе его заслуг — разработка логики Хоара (Hoare Logic), научной основы для конструирования корректных программ, используемой для определения и разработки языков программирования. Хоар создал ряд трудов по созданию спецификаций, проектированию, реализации и сопровождению программ, показывающих важность научных результатов для увеличения производительности компьютеров и повышения надежности программного обеспечения.

Сегодня Хоар — сотрудник лаборатории Microsoft Research в Кембридже (Великобритания), куда он поступил в 1999 году, после того, как ушел на пенсию из Оксфордского университета в звании почетного профессора. Недавно королева Великобритании пожаловала профессору Хоару рыцарский титул за заслуги в области образования и компьютерных наук.

Профессор Бертран Мейер закончил Парижский политехнический институт, получил магистерскую степень в Стэндфордском университете, затем степень доктора в университете Нанси (Франция). Получил звание профессора по компьютерным наукам в Федеральном технологическом университете в Цюрихе (Швейцария). Член Французской технологической академии. Свою карьеру начал с руководителя научно-исследовательского подразделения компании Electricite de France. Позже создал компанию Eiffel Software. Издает журнал Journal of Object Technology (www.jot.fm), автор множества статьей по объектно-ориентированному программированию, технологиям и языку Eiffel.