Горячая дeсятка: Надежность

Компьютеры «виснут» и «падают». Это реалии нашей жизни. И происходит это чаще всего из-за ошибок в программах. Обычно последствия минимальны — крепкое слово и перезагрузка. Но если комплекс программ управляет сложной распределенной системой (например, движением самолетов в воздухе или медицинским оборудованием), ошибка может стоит больших денег и даже человеческих жизней. Нэнси Линч и Стивен Гарланд создают инструментарий для предотвращения подобных катастроф. Они надеются, что он поможет создавать программы, практически лишенные ошибок. Трудясь в лаборатории компьютерных наук Массачусетского технологического института (MIT), ученые создали новый алгоритмический язык и средства программирования на нем. Гарланд говорит, что все это для того, чтобы процесс создания программ стал «строже», стал похож на инженерные науки. Гражданские инженеры сначала строят модель моста и тестируют ее задолго до того, как начать строительство. Программисты, напротив, чаще всего начинают с цели и, после некоторого обсуждения, просто садятся и пишут код. Инструментарий, который разработали Линч и Гарланд, позволяет программистам моделировать, тестировать и делать выводы о программе задолго до ее написания. Этот подход уникален и сильно отличается от других подобных проектов, направленных на улучшение качества программного обеспечения и растущих в недрах компаний Microsoft, IBM и Sun Microsystems. Уникальность его в том, что он не только позволяет повысить качество продукта, но и облегчает и упрощает процесс собственно программирования. В основе подхода Линч и Гарланда к данной проблеме, как и ко многим другим, лежит абстракция. Разработку нужно начинать с высокоуровневого списка задач, которые должна решить программа. Затем следует создание все более детальных установок, которые описывают как шаги, предпринимаемые программой для достижения поставленных целей, так и методы реализации таких шагов. Например, высокоуровневая абстракция для системы избежания столкновений самолетов в воздухе должна указать, какое исправляющее действие следует предпринять, если два самолета летят слишком близко друг к другу. Более низкий уровень мог бы включать обмен сообщениями между самолетами для определения того, кто из них должен подняться выше, а кто опуститься ниже.

Но Линч и Гарланд развили идею абстракции гораздо дальше. Лет десять назад Линч разработала математическую модель, которая облегчала задачу выяснения, будет ли набор абстракций, сформулированный программистом, правильно работать в распределенной системе. На базе этой модели Линч и Гарланд создали алгоритмический язык, на котором можно писать «псевдокод», описывающий, что же должна делать программа. При помощи своих студентов Гарланд также построил инструментарий, который позволяет доказать, что абстракции низкого уровня правильно соотносятся с абстракциями более высоких уровней, а также эмулировать поведение программы до того, как она превратится в настоящий код, например, на языке Java. Идея заключается в том, что внимание программиста привлекается к обстоятельствам, которые потенциально могут привести к ошибкам. Так инструментарий способствует тому, что программы будут всегда работать как задумано. После тестирования таким способом человек легко может превратить псевдокод в программу на одном из стандартных алгоритмических языков. Не все ученые-компьютерщики согласны с тем, что можно доказать безошибочность программы. Тем не менее специалисты отмечают, что подобные методы имеют право на существование и их использование для проверки критических мест большой системы полезно — вне зависимости от того, поможет ли это выявить 100% ошибок.

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

MIT Technology Review (c)2003