автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Развитие метода и инструментария многоуровневого доказательного проектирования программ

Академия наук Украины Институт кибернетики имени В.М. Глушкова

На правах рукописи БАКУЛИН Александр Владимирович

УДК 681.3.06

РАЗВИТИЕ МЕТОДА И ИНСТРУМЕНТАРИЯ МНОГОУРОВНЕВОГО ДОКАЗАТЕЛЬНОГО ПРОЕКТИРОВАНИЯ ПРОГРАММ

05.13.11 - математическое и программное обеспечение вычислительных машин, комплексов, систем и сетей

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

Киев 1992

Работа выполнена в . Институте кибернетики

имени В.М. Глушкова АН Украины

Научный руководитель: доктор технических наук

ЦЕЙТЛИН Г.Е.

Официальные оппоненты: член-корреспондент АН Украины,

доктор физико-математических наук Летичевский A.A.

кандидат физико-математических наук Каюров В.Ю.

Ведущая организация: Киевский государственный университет

им. Т.Г. Шевченко

Защита состоится " ¿У^/тСИ?*j> 1993 г. в /f' часов

на заседании специализированного совета 016.45.01

при Институте кибернетики имени В.М. Глушкова АН Украины по адресу:

252207 Киев 207, проспект Академика Глушкова, 40

С диссертацией можно ознакомиться в научно-техническом архиве Института

Автореферат разослан " 199j£ года

Ученый секретарь специализированного совета кандидат физико-математических наук

В.Ф.Синявски

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность проблемы. Создание надежного программного обеспечения (ПО) остается одной из нерешенные проблем современного программирования. Существенное влияние на надежность оказывают ошибки проектирования, являющиеся наиболее дорогостоящими и трудноустранимыми. В связи о этим достаточно остро стоит вопрос обоснования правильности проектов программ. На протяжении ухе многих лет развиваются и совершенствуются подходы, при которых программирование рассматривается как определенный вид математической деятельности: конструктивное определение функций в функциональном и композиционном программировании, построение аксиоматических систем в алгебраическом, концептуальном, логическом программировании, разработка математических моделей предметных областей в методах формализованных технических заданий, VDIí, Z, формальные преобразования математических описаний в трансформационном программировании. В рамках формальных методов программирования целесообразно рассматривать и задачу проверки проектов программ.

Одно из направлений современного программирования, основанное на применении алгебраических методов, сформировалось как результат развития теории систем алгоритмических алгебр (CAA) В.М.Глушкова и ее приложений . Аппарат CAA при соответствующей интерпретации носителей и операций применяется для многоуровневого проектирования программ; модифицированные системы алгоритмических алгебр (САА/Ы) дополнительно предоставляют средства описания параллелизма; в алгебре отруктур данных (АСД) - переинтерпретации CAA/U определен достаточно гибкий и выразительный формализм для опиоания и многоуровневого проектирования структур данных. Особенность рассматриваемого математического аппарата оостоит в возможности компакт-

него структурированного представления схем программ и данных в виде формул, для которых отработана техника тождественны! преобразований.

Аппарат САД/М положен в основу метода многоуровневогс структурного проектирования программ (МСПП), сочетающего алгебраические методы с формальными моделями языков. Инструментарий МСЛП - система »ШЪТИПРОЦЕСОИСТ - применялся к решенго задач различных классов и продемонстрировал повышение надежности и сокращение времени отладки разрабатываемых программ. Представляется полезши.! развитие метода МСПП в ориентации ш доказательное проектирование, вовлечение в область его действия начальных втапов жизненного цикла ПО. Это требует создания соответствующего математического аппарата, который можег быть получен в результате интегрирования СМ/М и АСД.

Целью диссертационной работы является построение теоретических и инструментальных средств, обеспечивающих обоснован» правильности проектов программ с применением верификации н етапе проектирования, что предполагает создание на основе ин тегрирования САА/М и АСД математической модели для представ ления проектов программ, формализацию понятия правильност проекта и построение математического аппарата для ее формаль ного обоснования, реализацию программных средств, поддерживг вдих доказательное проектирование.

Научная новизна работы состоит в следующем: - построен логико-алгебраический аппарат, ориентированный i многоуровневое доказательное проектирование программ, на о; нове которого:

1) развит подход к разработке проектов программ и определен] семантики абстрактных преобразователей данных, используем! при проектировании;

2) формализовано понятие проекта программы и его правильное и разработаны методы анализа проектов программ: тестировэни

верификация, трассировка (символическое выполнение); 3) построено исчисление, предназначенное для формального доказательства правильности проектов программ, доказаны теоремы о полноте и непротиворечивости исшсления, разработаны стратегии верификации проектов программ;

- предложен основанный на применении созданного математического аппарата метод многоуровневого доказательного структурного проектщ эвания программ (МСПП/Д), сочетающий многоуровневую модель .жизненного цикла ПО с обоснованием проектов на каагдом из уровней в соответствии с предложенными методами: тестирования, трассировки, верификации;

- в рамках создания программного обеспечения метода МСПП/Д определена понятийная основа 'языка (САА-спецификаций) формализованных спецификаций и разработан проект инструментария, который представлен средствами этого языка.

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

Простота и наглядность используемых средств, сочетающаяся с достаточной математической строгостью основных* концепций, создает предпосылки для использования метода МСПП/Д при обучении формальным методам программирования.

Инструментарий метода МСПП/Д реализован в рамках развития РИТМ-технолопш, проводимого в соответствии о Белорусской республиканской комплексной научно-техничеокой программой "Информатика" (номер гос. регистрации 01.90.0 036397).

Публикации и апробация работы. Приведенные в работе ре-

зультаты получены автором самостоятельно и докладывались на Всесоюзных семинарах "Параллельное программирование и высокопроизводительные системы" (Бердянск, 1936 г., Алушта 1988 г., Планерское 1989 г.) II-ой Всеооюзной конференции по прикладной логике (Новосибирск, 19S8), на семинаре отдела автоматизации программирования в ИК им. В.М.Глушкова АН Украины (1992 г.).

По теме диссертации опубликовано 9 работ.

Структура и объем работы. Работа состоит из введения, четырех глав, заключения, списка литературы из 127 наименований и двух приложений. Использованы 2 рисунка и 3 таблицы. Основной машинописный текст (без прилокений) составляет 115 страниц.

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ

Во введении обосновывается актуальность проблемы, определяются цели диссертации. Дается определение и краткая характеристика формальных методов (<Ш) программирования, в рамках которых проводится исследование. Сформулированы основные результаты, полученные в диссертации.

В первой главе рассматриваются языки формальных спецификаций (ЯФС), являющиеся основой £¡<1, формулируются некоторые требования, которым должны удовлетворять ЯФС. Проводится обзор средств САА/М и АСД с целью последующего развития на их основе формального мгтода програшированпя. Приводятся определения основных понятий САА/М и АСД, анализируются возможности, связанные с их применением в разработке ПО. Обосновывается способ интегрирования САА/М и АСД, обусловленный их приложением к доказательному проектированию программ.

В диссертации определены следующие требования к ЯФС: 1) наличие средств структуризации и декомпозиции; 2) поддержка различных методов (модельных, аксиоматических) спецификации и

возможность выбора наиболее подходящего из них в каждом конкретном случае; 3) наличие формальной системы, ассоциированной с ЯФС и предназначенной для исследования свойств спецификации; 4) использование в спецификациях неформальных пояснений.

Модифицированная система алгоритмических алгебр (САА/М) -это тройка <U,V;0>, где элементы множества U (операторы) -отображения информационного множества М (совокупности состояний абстрактной вычислительной машины) в себя, элементы множества У (условия) - отображения М в трехзначное множеотво логических значений Bool, а сигнатура операций Q включает операции: композиция - А*В - последовательное выполнение операторов А и В; а-дизъюнкция - (а:А\В) - конструкция типа if а then A else В; а-итерация - {а:А} - конструкция типа while -.а do А; фильтр - [а] - конструкция типа if a. then skip else abort и др. (кроме goto). Алгоритм сортировки вставками, например, в САА/М представляется так, как это показано в отроке 1 таблицы 1 (стр. 10), где INIT - оператор, устанавливающий указатель ! в начало массива, SHF - оператор сдвига указателя ! вправо по массиву, INS - оператор установки элемента, расположенного слева от указателя !, в уже упорядоченную часть массива таким образом, чтобы упорядоченность сохранялась, Endarr - условие, истинное, когда весь массив обработан.

К основным понятиям алгебры структур данных (АСД) относятся: конфигурация - цепочка символов некоторого алфавита, объект - множество конфигураций, применение объекта (в режиме распознавания) - проверка принадлежности конфигурации объекту. Носителями в АСД считаются объекты и условия, определенные на (размеченных специальными символами) конфигурациях. Сигнатура операций АСД и САА/М совпадает, но в случае АСД операции определяются над объектами. Чтобы задать в АСД структуру цепочки, следует указать формулу, представляющую раопо-

знающий оту цепочку объект. Например, формула из таблицы 1 (строка 3), где конфигурации объекта Real - действительные числа, задает числовую последовательность (массив). По определению, на каждом шаге ос-итерации распознается одна конфигурация объекта Real, и процесс завершается, когда будет распознана последовательность конфигураций из Real (станет истинным условие eoíarr»). Формулы АСД подобным образом позволяют определять достаточно ело same структуры данных.

В целях доказательного проектирования предлагается переинтерпретировать информационное множество САА/М, используя для ©того средства АСД. Это обеспечит: структурированность, строгость описания и верифицируемость проектов программ; возможность декомпозиции решаемых задач в результате применения иерархически связанных формул САА/М и АСД; легкость обучения, обусловленную единообразием средств представления алгоритмов и данных.

Во второй главе в результате интегрирования САА/М и АСД, развития их изобразительных возможюстей на основе расширения нотации, уточнения существующих и ¿¡ведения ног х понятий строится логико-алгебраическая модель, ориентированная на создание многоуровневых проектов программ. Предлагаемый математический аппарат предоставляет средства для описания и многоуровневого проектирования алгоритмов и данных, а такке специальные логические средства представления семантики абстрактных примитивов, испс *ьзуемых при проектировании. Разрабатывается концепция к-интерпретации как инструмента определения функциональных спецификаций, формализуется понятие проекта программы и определяется порядок разработки проектов. Формируется понятийная основа языка спецификаций и проектирования программ.

Инструментом многоуровневого проектирования алгоритмов и данных являются совокупности последовательно уточняющих друг

б

друга формул САА/М и АСД, образующие операторные и объектные схемы и определяемые в диссертации таким образом. Объектной схемой называется совокупность равенств вида О =]? (1=1..п), где С^ — объекты, Р - формулы АСД, такие что в левой части каждого равенства (кроме первого) мозсот находиться только такой объект 01, который уке встречался в формуле (формулах) предыдущих равенств. То ость, каждое последующее равенство конкретизирует посредством формулы АСД объект из предыдущего равенства, что обеспечивает многоуровневость представления. Аналогично определяется операторная схема, но с дополнительным требованием отсутствия рекурсии. При етсм операторы рассматриваются как отображения на множестве кортежей помеченных конфигураций ЛСД, называемых ^конфигурациями. Проводимое таким образом интегрирование САА/М и АСД обеспечивает возможность взаимобвязанпого описания алгоритмов и данных.

В диссертации развивается специальный математический аппарат, сочетающий средства АСД и формальной логики с целью денотационного представления функций, в частности операторов САА/М. Центральное место в нем занимает понятие к-штерпре-тации, которая представляет собой задаваемый специальным образом двуместный предикат, устанавливающий области определения и значений соответствующей функции, а также связь мезгду входными и выходными значениями. Предикат строится тактах образом, что значением его является "истина", когда конфигурации, являющиеся в совокупности аргументами предиката, имеют задаваемую объектными схемами структуру. Построение рассматриваемого аппарата требует расширения изобразительных возможностей АСД. С етой целью вводятся переменные, которые позволяют формулировать сложные логические условия. Запись вида О-о устанавливает, что распознаваемая в момент применения объекта О конфигурация, обозначается переменной применения объекта с. Если о - переменная применения объекта, применяемого в теле

цикла, то o(i) обозначает конфигурацию, распознаваемую объектом С при 1-той итерации тела цикла. Точкой обозначается номер текущей итерации, который считается равным О перед началом выполнения цикла и увеличивается на 1 поело проверки условия выхода из цикла, если значение•условия "ложь".

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

Выражение Р(х ,х„,...,х ) вида х ::0 .х ::0.....,х ::0 ,

12 n 1 12 2 ' «» п

принимающее логическое значение "истина" (1), если для любого I конфигурация Xj распознается объектом 0(, к логическое значение "ложь" (О) .в противном случае, называется к-предикатом. Переменные применения объектов в к-предикатах считаются свя-закнши квантором существования. Ю-предикат

K.f(xi,x^,...,xn,y) a i(xt,хя,...»Хп)=У называется к-интер-претаци^й функции i(xi$xn>....х^). Функции можно задавать либо определяя к- интерпретацию в явном виде, либо применяя аксиоматический подход и связывая к-интерпретации соотношениями. В строках 5-0 таблицы 1 представлена к-интерпретация фуя-кчдо soi-t, сортирующей числовой массив (при этом используется функция о«опюЬ(х,у), устанавливающая число вхождений в массив у. некоторого элемента у; к-интерпретация occnmb приведена в диссертации). Содержательно K.eort(x;y) означает следующее: в результате применения фун^сции sort"к конфигурации х будет.получена конфигурация у, если существуют конфигурации z, i? та--кие, что х распознается объектом, представленным формулой, указанной после х::, и (одновременно) у распознается объектом, представленным формулой, указанной после у::. -

Логически связанные понятия (функции) и объекты объединяются в классы, представляющие собой пары вида-(О,?), где О -

множество объектов, Р - множество определенных на множестве О функций. В строках 2-8 таблицы 1 описан масс Array, определяющий числовые массивы и функции, применяемые к ним. В терминах функций классов представляется семантика операторов САА/М, формализуемая следующим образом.

К-предикатом по множеству меток N называется выражение Р„(х) вида il :;0,,...,N ::0 , принимающее логическое значение

N - I I ею

"истина", если в к-конфигурации х имеются конфигурации с меткамч N(€ N и каждая из них распознается соответствующим объектом Оt (i=1..m), и логическое значение "ложь" в противном случае. К-конфпгурация u=PM M(x,y)/t о множеством меток конфигураций N называется сечением двуместного к-предиката Рн м(х,у) по к-конфигурации t, если Рн M(t,u)=1. По определению, Р„ „(z,y)/t=laindf, если vy: P„ „(t,y)*1, где kundl обо-

п l N К (К

значает неопределенную к-конфигурацию.

j»

К-интерзретацией оператора А (обозначается через А) называется двуместный к-предикат Р„ „(х,у) по множествам меток II

Н IN

и N, такой что:

1) Рн,ы(х,у) & Рм,н(2'2' ♦ (y=2)i

2) vb е Ei : А(е)=в®РЧ1Н(х,у)/е;

где 1Ш - множество к-конфигураций, в - операция наложение, определяемая так, что х«у есть объединение к-конфигураций х и у, из которого исключены помеченные конфигурации, принадлежащие х, с метками из пересечения множеств меток, используемых в х и у. Из определения к-интерпретации следует, что результатом выполнения некоторого оператора является наложение ое-чення его к-интерпретации на входные данные. В отроках 9-12 таблицы 1 в качестве примера приведены к-интерпретации операторов схемы SORT. (Обозначение <о> попользуется для объекта, содержащего только одну конфигурацию с).

Если kA=P„ „(х,у)= Ы,::о",...,М ::0M;N ::0",..,N ::0М , то

n|N 1 1 и . n 1 1 п п<

к-предикат ?Рм(х)=М ::0";,...,М ::0 называется входным прел 1 1 ■ П А

дикатом оператора Л, к-предикат Р ?(x,y)=N ::0" -

N 11 n п

выходным предикатом оператора А, а операторная формула А=[?Р]*А*[Р?] - к-тройкой оператора А, которая является другой формой представления к-кнтерпретации.

Используя введенные понятие:, проекты программ предлагается задавать в форме проектных спецификаций - троек вида <S; {Cj}; {К(}>, где S - операторная схема, Cj - классы, К - к-китерпретации операторов и условий схемы S, при определении которых использованы введенные в классах Gt функции. При разработке представляемых таким образом проектов следует описать алгоритм решаемой задачи (в форме операторной схемы), обрабатываемые данные (в форме объектных схем), понятия предметной области (в форме функций классов) и функциональные спецификации (в форме к-инторпретаций) программы и ее составных частей (отождествляемых с операторами САА/М). Математическая строгость применяемых при проектировашм средств обеспечивает возмоаиооть проверки (формальной в том числе) проектов программ. Пример проектной спецификации представлен в таблице 1.

— Таблица 1. Проектная спецификация программы сортировки —

1. <SORT=IKIT * (Endarr: SIII»1 * INS } ;

2. С КЛАСС Array =

3. = (coiarr: Real}

4. sort: Array -> Array

5- K.sort(x;y) - x::feoiarr: Real-z},

6. y:: (eoiar-r: Real-r * [(.>1) -> (r(.)> r(.-1))]} *

7. * [vi>1: oocmb(x,r(i))=oocnmb£y,r(i))) &

8. & ooonmb(x,a(i))=осопиЬ(у,ц(1))] }

9. CSORT= A::Array-x; A::Array-y * [K.cort(x;y)i.

10. *ШГГ= A::Array-x; A::<!> * <x>.

11. SilP- a: :Array-x*<!>*Real-r*Array-y;A: :<x>*<r>*<!>*<y>.

12. KINS= A::Arr-sy-x *<!>*Real-r* Array-y * [K.sort(x;x)];

A::Array-z * <!> * <y> * [X.üort(xr;c)] }>

Средства САА/М и АСД, дополненные рассмотренными понятиями, образуют в совокупности понятийную основу языка формализованных спецификаций и проектирования (далее язык САА-спецификаций). В силу особенностей применяемого математичес--

:<ого аппарата этот язык является императивно-декларативным, обладает развитыми механизмами структуризации и декомпозиции, предоставляет средства для построения модельных и аксиоматических спецификаций, включает в себя небольшое число базисных понятий и обозначений, что упрошает его изучение.

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

Тестирование проектных спецификавдгй обеспечивается формализацией попятил выполнения оператора САА/М. Подавая на вход операторной схемы К к-конфигурацаю е и применяя к ней операторы схемы в соответствии о та к-интерпретациями и в порядке, определяемом логикой схемы, на выходе получим к-конфигуращзэ 1;. Из определения к-интерпретации следует, что в проектной спецификации олибки отсутстукт, если выполняется условие з®кй/з-с. Тестирование проектных спецификаций является многоуровневым, так как проводится отдельно и независимо для кааг-дого равенства операторной схемы.

Назовем согласованным операторное равенство, к-интерпрета-ции левой и правой частей которого равны. Операторная схема согласована, если согласованы все ее. равенства. Правильность проектов отождествляется с согласованностью операторных схем. Б результате задача обоснования правильности проектов сводится к построению и сравнению к-интерпретаций.

Для проведения формального обоснования правильности проектов (верификации) предлагается исчисление к-интерпретирован-ных схем Термами в £ считаются формулы САА/М; правильно построенными формулами - к-интерпретированные формулы САА/М, в которых на месте операторов стоят их к-тройки; аксиомами -

к-тройки операторов исследуемой схемы; правила вывода (таблица 2) определяют к-инт^рпретации операций САА/М.

-Таблица 2. Правила вывода исчисления £---

«п. ?*А*В*0, К/а=кА/в»кВ/(е»кА/с)

СК- -р*тнА*ь)иде-

. Р*(а: А\В)*0* П/е;;(д: <кА/е>\<кВ/в:>)

в - произвольная к-конфигурация; Н - к-предикат по множеству меток; А,В - произвольные, Е- тождественный, N - неопределенный операторы;а - условие; формула исчисления или тождественный оператор; А - композиция из 1 операторов А.

Доказаны следующие теореыы, характеризующие исчисление £.

Пусть далее Р - операторная формула, Р - соответствующая ей к-интерпретированная формула, И - к-предикат.

ТЕ0Р5МА ^ (о непротиворечивости исчисления). Если в исчислении £ из Р выведены к-тройки [?Р]Р[Р?] и то

«V

ТЕОРЕМА 2. Если в исчислении £ из Р выводима формула [?ЯМ11?1, то И - к-интерпретацая р.

Операторная формула принадлежит классу к-интерпретируемш операторных формул К, если для любой ее подформулы существует к-интерпретация. *

ТЕОРЕМА 3 (о полноте исчисления). Если Р принадлежит классу К, И - к-интерпретация Р, то в исчислении £ из Р выводима формула 1?11ШН?].

Из теорем 2 и 3 и определения согласованности операторных равенств следует теорема 4.

ТЕОРЕМА 4. Операторное равенство А=Р, где Р принадлежит классу С, согласовано тогда я только тогда, когда в исчислении £ из Р выводима формула [?кА]Р1КА?].

При сверточной стратегии доказательства согласованности из формулы выбирается подформула, к которой применяется подходя-

цее правило вывода и получаемая в результате к-тройка под-

зтавляется в формулу вместо этой подформулы. Например, примел л

*ение правила вывода CR к комгозиции SHE1*INS в схеме SORT да-гт к- тройку:

[А:;Аггау-х*<!>*Real-r*Array-y * [K.sort(x.x)]] (SHF*INS) [A::Array-s * <!> * <y> * [K.sort(xf,z)]],

л л

которая затем замещает в формуле SHF*IN3. Равенство согласо-зано, если обрабатываемая формула преобразуется в к-тройку, соответствующую к-интерпрстации левой части равенства. В зависимости от направления сканирования формулы о целью приме-ie-ния подходящего правила вывода возмояэкы левосторонняя, пра-зосторонняя, левосторонняя и правосторонняя поочередная (сменянная) и одновременная (параллельная), стратегии верификации.

Разверточная стратегия применима, если обрабатываемую формулу можнб представить в виде композиции А*В так, чтобы по известным ^(А*В) и 1гА' определить кВ. Если В оператор, то вышеленная к-пнтерпрбтация оператора В сравнивается с заданий; в противном случае "разворачивается" В: формируется ком-

v k: к

юз1щия В=С*В о известной к-интещретацкей С, по В и С вы-

v

отеляется D и т.д. Доказательство счигаетсл успешным, если see к- интерпретации, полученные в процессе развертки, совпадают с заданными. Разверточная стратегия полезна в сочетании го сверткой.

Трассировка проектных спецификаций близка в идейном плане гимволическому выполнению программ. В соответствии о некоторым критерием обоснования в операторной схеме выбирается ?расоа - последовательность операторов, получаемая в резуль-?ате назначения определенных значений условиям формул. Строи-?сл к- интерпретация трассы. К-интерпретация. схемы R опреде-шет к- интерпретацию любой трассы Т, по&тому должна выполня-?ься импликация kT->kR, - в противном случае в проекте еодор-сатся ошибки..

В четвертой главе на основе предложенного ' математическое аппарата разрабатывается метод доказательного многоуровневое структурного проектирования программ (ЫСПП/Д) к поддерживающий его инструментарий (система САА/ПРОЦЕССИСТ)-. Обсуздактс. сферы приложения и перспективы развития рассматриваемого подхода.

-Таблица 3. Разработка программ по методу МСПП/Д-

1-й уровень

.ппсг.пковка. задачи, проектирование алгоритма. и данных -разработка объектных и операторных ехал, классов; .разработка т-иктсрпреглаиуй (стилизованных описаний на естественном языке) примитивов проектной спецификации; .согласование: тестирование, трассировка, верификация т-интерпретироваыных схем.

2-й уровень

,р2зработка к-шаперпретациЛ. примитивов проектной спецификации на основе их т-интерпретаций;

.согласованиетестирование, трассировка, верификация к-ин-терпретированных схем.

3-й уровень

.разработка п-интерпретащй -- программных реализаций примитивов проектной спецификации - ка основе их т- и к-интер-претаций;

.согласование: отладка программы - пооператорное (в слысле СЛА/М) выполнение програлжи, сгенерированной по операторной стеле и заданны* реализация* операторов, на тестовых наборах данных.

Метод МСПП/Д основан на той же идеологии разработки ПО что и метод МСПП (многоуровневое проектирование схемы программы средствами САА/М, программная реализация базиса, генерация программы по схеме и программным фрагментам, соответст вующим базису). Наряду о отим расширена область жизненно!', цикла ПО, охватываеиая методом: функциональная спецификаций верификация проектных спецификаций, тестирование и отладка систематически применяются как неформальные, так и формальны! спецификации; в целях доказательного проектирования применяется многоуровневая ыо.цель жизненного цикла ПО. Разработка программ по иетоду МСПП/Д проходит через тти последователь»

гочняющих друг друга уровня, отличающихся способ ом интерпре-ации операторов, условий, функций (далее примитивов) проект-ой спецификации (табл1ща 3) •

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

Отличительные черты системы САА/ПРОЦЕССИСТ, являющейся ра-(витием системы МУЛЬТИПРОЦЕССИСТ, ето: трехуровневая модель жизненного цикла ПО,, на каждом из которых выполняется проце-iypa обоснования согласованности; диалоговый интерфейс; применение синтаксически-ориентированных редакторов для ввода зхем и интерпретаций; применение двух языков (подмножеств зходного языка системы ГШЬТКПРОЦЕССИСТ) для представления жераторных схем; развитая справочная служба. Поддерживаемые системой САА/ПРОЦЕССИСТ ©таны разработки программ по методу .'.СПП/Д выделены в табЛ1ще 3 курсивом. В текущей версии система САА/ПРОЦЕССИСТ ориентирована на создание программ на языке REXX в среде ПДО СЕМ. Система включает в себя 37 программ, написанных на языках REXX и ЕХЕС2 (общий объем около 5 тыс. строк), использует редактор XEDIT ПДО СВМ и средство управления экраном дисплея - пакет EMS CMS.

В приложении 1 приведены доказательства свойств исчисления к-интерцретированных схем. В приложении 2 содержится проектная спецификация системы САА/ПРОЦЕССИСТ.

ЗАКЛЮЧЕНИЕ Перечислю/ результаты диссертации, выносимые на защиту.

1. Построена логико-алгебраическая модель, ориентированная на ооздание многоуровневых проектов программ, на основе которой:

- о применением введенных понятий (к-предиката, сечения к-предиката, класса и др.) и сформулированной концепции к-интерпретации, развит подход к разработке проектов программ и определению семантики абстрактных преобразователей данных, используемых при проектировании;

- предложен формализм проектной спецификации в качестве средства представления проектов программ;

- формализованы семантика выполнения оператора алгебры алгоритмов, понятие правильности проекта программы и разработаны методы анализа проектных спецификаций: тестирование, верификация, трассировка (символическое выполнение).

2. Построено ассоциированное с предложенной моделью исчисление к-интерпретированных операторных схем, аксиомами в котором считаются к-интерпретации (функциональные спецификации) операторов алгебры алгоритмов, а правила вывода характеризуют свойства операций алгебры алгоритмов. Доказаны теоремы о полноте и непротиворечивости исчисления и показано, что доказательство правильности проектов программ сводится к выводу формул исчисления. Предложены различные стратегии проведения формального доказательства: оверточная, разверточная, смешанная (в том числе параллельная).

3. На основе созданного математического аппарата разработан метод многоуровневого доказательного отруктурного проектирования программ (ЫСПП/Д), в котором попользуется многоуровневая модель жизненного цикла ПО и на каждом из уровней проводится проверка проектов разрабатываемых программ с применением предложенных методов тестирования, верификации и трассировки проектных спецификаций.

U В рамках создания программного обеспечения метода ЫСПП/Д: - определена понятийная основа языка (САА-спецификаций) спе-(ифйкации и проектирования программ декларативно-мперативного типа с развитыми изобразительными возможностями [ля представления модельных и аксиоматических спецификаций; ■ разработана и представлена средствами языка САА-пецификаций проектная спецификации инструментария ЫСПП/Д. '. В рамках развития РИТМ-технологии, проводимого в соответс-вии о Белорусской республиканской комплексной научно- техни-еской программой "Информатика" (номер гос. регистрации >1.90.0 036397), реализован инструментарий, поддерживающий сновные втапы разработки программ по методу МСПП/Д.

Основные положения диссертации опубликованы в работах:

1. Бакулин A.B., Грицай В.П., Моравский P.P. Организация налога в системе МУЛЬТИПРОЦЕССИСТ // Организация взаимодейо-вия человека с ЭВМ : Сб. научных трудов. - Киев, 1985.- С. 2- 23.

2. Бакулин A.B. О реализации языка управления системой УЛЬТИПРОЦЕССИСТ // 7-я Всесоюз. шк.-семинар "Параллельное рограммирсвание и высокопроизводительные системы": Тез. экл.- Киев, 1986.- С. 52-53.

3. Костырко B.C., Бакулин A.b. Об индуктивном сш1тезе ин-эриантных утверждений и функций программ // Кибернетика.-J86.-N1.- С.18-24.

4. Бакулин A.B. Об организации архива системы МУЛЬТИПРО-2ССИСТ // 8-й Всесоюзный семинар "Параллельное программиро-шие и высокопроизводительные системы": Тез. докл.- Киев, J88.- С. 56-57.

5. Бакулин A.B., Цейтлин Г.Е. Об одном подходе к алгебраи-)ской спецификации программ // 2-я Всесоюз. конф. по прикла-юй логике. Новосибирск, 7-9 июня 1988 г.: Тез. докл.- Но-

восибирск, 1980.- с. 234-236.

о. Бакулин A.B., Об одном подходе к спецификацш1 и проект: ровашяо программ // 10-я Воеооюз. шк.-семинар "Параллельн программирование и высокопроизводительные системы": Те докл.- Киев, 1990.- С. 61-62.

7. Бакулин A.B. Математическая модель языка спецификаций проектирования программ.- Мн., 1991.- 25с.- (Препринт / БССР. Вычислительный центр; N 4(4)).

8. Бакулин A.B. Многоуровневая разработка программ, оси ванная на применении интерпретированных схем алгебры алгор тмов .-Мл., 1991.- 23с.- (Препринт /АН БССР. Вычислитель! центр; N 5(5)).

9. Цейтлин Г.Е., Бакулин A.B. Многоуровневые структурщ ванные проекты программ и их обоснование // 1Сибернетика системный анализ.- 1991.- N5.- С. 98-107.