Использование формальных методов в программировании © 1998 Серж де Арт (Сергей Свистунов) Тезисы к 5й научной конференции «Современная логика: Проблемы теории, истории и применения в науке», Спб., 1998 Программирование, как область человеческой деятельности, возникло вместе с появлением компьютеров. Выйдя из стен научных лабораторий, оно быстро превратилось в огромный, динамично развивающийся мир. Сложилась определенная культура создания программ и их эксплуатации. Слабой стороной этого естественого и поэтому «плохо контролируемого» процесса стало, например, то, что пользователи постепенно привыкают к таким вещам, как недоработка программ, «зависания» компьютера, и даже не очень качественные операционные системы. Мы вправе задаться вопросом в духе Лейбница — «является ли этот комьютерный мир наилучшим из возможных?» Или, другими словами, в какой степени цифровые технологии использовали и используют результаты прикладных и фундаментальных наук? Помимо массового использования компьютерных систем есть сферы применения, где требуется повышенная надежность и безопасность, и где даже небольшой сбой может повлечь за собой людские, финансовые и иные крупные потери. В отличие от объектов физического мира, программные продукты не изнашиваются, и в этом смысле являются вечными. Любая неисправность в системе — это всегда ошибка, допущенная при ее разработке. Можно использовать различные методики для решения этой проблемы, такие как тестирование, дублирование задания среди разработчиков, или попытаться априорно предотвратить неисправность. Как показала практика, самым обнадеживающим оказывается последний подход. Среди имеющихся в рамках этого подхода техник, Формальные Методы (далее FM) оказались наиболее сильными, и поэтому наиболее многообещающими. Разработчик некоторой системы, прежде чем браться за ее создание, обдумывает и фиксирует (на бумаге) ряд требований, которым должна отвечать его система. На этом этапе пропуски и неточности в определениях могут иметь серьезные последствия на дальнейших стадиях разработки. Спецификации, написанные на естественном языке и сопровождаемые полуформальными диаграммами и иллюстрациями, могут оказаться двусмысленными и даже противоречивыми. Поэтому первым шагом, где FM могут оказать помощь, является 1. уровень спецификации системы. Данный уровень характеризуется использованиеи математической логики для описания: допущений относительно мира, в котором система функционирует требований, которым система должна отвечать проекта, отвещающего этим требованиям 2. Уровень формальной разработки системы. Для него характерно использование «бумажных» доказательств. 3. Формальная верификация системы. Используются программы автоматического доказательства теорем. Для этого уровня характерно наиболее строгое применение формальных методов. В данном контексте представляют интерес семантические и дедуктивные таблицы логика и философа Э.В.Бета, а также его идеи о «машинах доказывающих теоремы» (1). Идеальным случаем является использование FM на всех трех уровнях. Однако, их применение только к наиболее критическим частям системы также является выгодной стратегией. Общим свойством для различных FM является то, что все они обладают следующими атрибутами: они основаны на логике, используют понятия языков программирования (типы данных, модульные структуры, и.т.д.), способны выражать нечто без объяснения того, как это реализовано (т.е непроцедурный подход), содержат формальную семантику, допускают возможность построения инструментальных средств пригодных для анализа. Еще в середине 80х гг. FM использовались в основном как средства верификации для доказательства корректности программ применимых только к «игрушечным» задачам. Начиная с 90х гг. наметился явный прогресс. Их использование в промышленности постоянно расширяется, и что самое интересное, меняется отношение к FM со стороны разработчиков-скептиков. Организации, ответственные за расширение применений FM, признали их перспективность и применимость. Например, в Европе программу распространения FM поддерживает комиссия ЕС. Важной вехой в развитии FM стало событие 1993 года, когда группа экспертов по FM провела международное исследование по применению FM в промышленности. Объем отчета (2) составил более 300 страниц. Для анализа были отобраны 12 успешных проектов из разных областей применения, в которых использовались разные методы и разные инструментальные средства. Были сделаны интересные обобщения. А на основе интервьюирования разработчиков и заказчиков (Европы, США и Канады) были сформулированы дальнейшие перспективные направления развития FM. Среди них можно выделить следующие: усовершенствование интеграции FM с другими техниками разработки программного обеспечения, совместное развитие с такими технологиями как визуализация, мультимедия и объектно-ориентированное программирование, включение систем реального времени, параллельных систем и асинхронных процессов. Сегодня основными областями промышленного применения FM служат: управление и контроль за движением (воздушного) транспорта, Case-технологии, информационные, железнодорожные и медицинские системы, сетевое администрирование, разработка программного обеспечения (в том числе для космоса), телекоммуникации и сетевые протоколы, системы обработки транзакций и.т.д. Перечень общеизвестных FM составляет более 40, а инструментальных средств более 60. Наиболее типичными формальными методами являются: VDM, Z, RAISE и LOTOS. В последнее время специалисты по FM стали активно задумыватья над причинами того, почему инженеры (программисты) не проявляют интерес к этой технике, и порой даже избегают ее. Большинством исследователей было выдвинуто предположение, что причины, как правило, кроются в технических деталях и включают: отсутствие адекватных средств разработки, отсутствие хорошей математической подготовки у разработчиков, несовместимость с действующими техниками, дороговизну создания. Другие видят причину в слабой аргументации, нацеленной на убеждение программистской аудитории. Как отмечает М.Халавей (3) «нежелание многих инженеров использовать или поддерживать развитие какого-либо FM или инструментального средства подсказывает другую возможную причину: вероятно проблема принятия лежит не в деталях, а в том способе, которым идея доводится до инженеров». Он настаивает на более безупречных в формальном отношении доказательствах. На мой взгляд, задача убеждения программистов в преимуществах использования FM, должна опираться на разработку эффективных аргументов именно для программистской аудитории. Аудитория программистов, несмотря на ее разнородность, является достаточно специфичной. Естественно, в первую очередь следует учитывать особенности конкретного человека, с которым состоится общение. Литература: E.W.Beth. Formal Methods. D.Reidel, 1962 An International Survey of Industrial Applications of Formal Methods. v.1-2, U.S. Department of Commerce, Technology Administration, National Insttitute of Standards and Technology, Computer Systems Laboratory, Gaithersburg, MD 20899, March, 1993 C.Michael Holloway. Why Engineers Should Consider Formal Methods. NASA Langley Research Center, Proceedings of the 16th Digital Avionics Systems Conference, October 1997 Usenet newsgroups: comp.specification.misc; comp.specification.z Санкт-Петербург, 18 апреля 1998 *