Введение к работе
Актуальность проблемы. Создание надежного программного обеспечения (ПО) остается одной из нерешенных проблем современного программирования. Существенное влияние на надежность оказывают ошибки проектирования, являющиеся наиболее дорогостоящими и трудноустранимши. В связи о этим достаточно остро стоит вопрос обоснования правильности проектов программ. На протякении ухе многих лет развиваются и совершенствуются подходы, при которых программирование рассматривается как определенный вид математической деятельности: конструктивное определение функций в функциональном и композиционном программировании, построение аксиоматических систем в алгебраическом, концептуальном, логическом программировании, разработка математических моделей предметных областей в методах формализованных технических заданий, VDIf, Z, формальные преобразования математических описаний в трансформационном программировании. В рамках формальных методов программирования целесообразно рассматривать и задачу проверки проектов программ.
Одно из направлений современного программирования, основанное на применении алгебраических методов, сформировалось как результат развития теории систем алгоритмических алгебр (САА) В.Ы.Глушкова и ее приложений . Аппарат САА при соответствующей интерпретации носителей и операций применяется для многоуровневого проектирования программ; модифицированные системы алгоритмических алгебр (САА/Ы) дополнительно предоставляют средства описания параллелизма; в алгебре отруктур данных (АСД) - переинтерпретации САА/М -~ определен достаточно гибкий и выразительный формализм для опиоания и многоуровневого проектирования структур данных. Особенность рассматриваемого математического аппарата оостоит в возможности компакт-
ного структурированного предотавленил схем програші и данных в виде формул, для которых отработана техника тождественных преобразований.
Аппарат САА/М положен в основу метода многоуровневогс структурного проектирования программ (МСПП), сочетающего алгебраические методы с формальными моделями языков. Инструментарий МСПП - система МУЛЬТШРОЦЕСОИСТ - применялся к решения задач различных классов и продемонстрировал повышение надежности и сокращение времени отладки разрабатываемых программ. Представляется полезным развитие метода МСПП в ориентации т доказательное проектирование, вовлечение в область его действия начальных втапов жизненного цикла ПО. Это требует создания соответствующего математического аппарата, который може' быть получен в результате интегрирования САА/М и АСД.
Целью диссертационнсй работы является построение теоретических и инструментальных средств, обеспечивающих обосновали правильности проектов программ с применением верификации н етапе проектирования, что предполагает создание на основе ин тегрирования САА/М и АСД математической модели для представ ления проектов программ, формализацию понятия правильнеет проекта и построение математического аппарата для ее формалъ ного обоснования, реализацию программных средств, поддерживг щнх доказательное проектирование.
Научная новизна работы состоит в следующем: - построен логико-алгебраический аппарат, ориентированный і многоуровневое доказательное проектирование программ, на ы нове которого:
-
развит подход к разработке проектов программ и определен] семантики абстрактных преобразователей данных, используем: при проектировании;
-
формализовано понятие проекта программы и его правильное и разработаны методы анализа проектов программ: тестировани
верификация, трассировка (символическое выполнение); 3) построено исчисление, предназначенное для формального доказательства правильности проектов программ, доказаны теореми о полноте и непротиворечивости исчисления, разработаны стратегии верификации проектов программ;
предложен основанный на применении созданного математического аппарата метод многоуровневого доказательного структурного проектщ звания программ (МСПП/Д), сочетающий многоуровневую модель ямзненного цикла ПО с обоснованием проектов на какдом из уровней в соответствии с предложенными методами: тестирования, трассировки, верификации;
в рамках создания программного обеспечения метода МСПП/Д определена понятийная основа 'языка (САЛ-спецификаций) формализованных спецификаций и разработан проект инструментария, который представлен средствами етого языка.
Практическая ценность. Метод МСПП/Д, иредлокенный е диссертации, иожет использоваться при разработке реальных программных систем и способствует повышению надеязгости создаваемого ПО. Это обеспечивается использованием предложенных методов обоснования правильности проектов программ п языка СМ-спецификаций, обладающего развитыми механизмами структуризации и декомпозиции, практическая пригодность которого была продемонстрирована при построении инструментария МСПП/Д.
Простота и наглядность используемых средств, сочетающаяся с достаточной математической строгостью основных» концепций, создает предпосылки для использования метода МСПП/Д при обучении формальным методам программирования.
Инструментарий метода МСПП/Д реализован в рамках развития РИТМ-технологии, проводимого в соответствии о Белорусокой республиканской комплексной научно-техничеокой программой "Информатика" (номер гос. регистрации 01.90.0 036397).
Публикации и апробация работы. Приведенные в работе ре-
зультаты получены автором самостоятельно и докладывались на Всесоюзных семинарах "Параллельное программирование и высокопроизводительные системы" (Бердянск, 1936 г., Алушта 1988 г., Планерсков 1989 г.) 11-ой Воеооюзной конференции по прикладной логика (Новосибирск, 19S8), на семинаре отдела автоматизации программирования в ИК им. В.М.Глушкова АН Украины (1992 г.).
По теме диссертации опубликовано 9 работ.
Структура и объем работы. Работа состоит из введения, четырех глав, заключения, списка литературы из 127 наименований и двух приложений. Использованы 2 рисунка и 3 таблицы. Основной машинописный текст (без прилоконий) составляет 115 страниц.
