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

гч.

£

чно-информационный центр проблем интеллектуальной собственности при министерстве общего и профессионального образования ^ Российской Федерации

Рязанская государственная радиотехническая академия

На правах рукописи

КАШИРИН Игорь Юрьевич

УДК 681.3.06:519.6

МЕТОДЫ ФОРМАЛЬНОГО АНАЛИЗА

ИНСТРУМЕНТАЛЬНЫХ СИСТЕМ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ ЭВМ НА ОСНОВЕ ТЕОРИИ УНИФИКАЦИИ

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

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

г.Москва 1997г.

Работа выполнена в Научно-информационном центре проблем интеллектуальной собственности (НИЦПрИС) г.Москва (Рязанский отдел НИЦПрИС при Рязанской государственной радиотехнической академии).

Научный консультант: Заслуженный деятель науки и техники России, д.т.н., профессор Коричнев Л.П.

Официальные оппоненты:

доктор технических наук, профессор Петров О.М. доктор технических наук, профессор Савельев А.Я. доктор технических наук, профессор Саксонов Е.А.

Ведущая организация:

Институт программных систем Российской академии наук

Защита состоится "/У 1997г. в 12 часов

на заседании Специализированного Совета Д063.93.01 Московской Государственной академии приборостроения и информатики (МГАПИ) по адресу: 107076, г.Москва, ул.Стромынка. д.20.

С диссертацией можно ознакомиться в библиотеке Московской Государственной академии приборостроения и информатики.

Автореферат разослан " " /¿¿у^А-* 1997г.

Ученый секретарь Специализированного Совета Д063.93.01 МГАПИ

к.т.н., доцент -----Ульянов М.В.

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

Актуальность проблемы

Со времени появления первых инструментальных средств программирования - программирующих программ и простейших алгоритмических языков до текущего момента программный инструментарий прошел несколько этапов существенных качественных изменений. Наряду с языками программирования (ЯП), пакетами прикладных программ и проблемно-ориентированными библиотеками готовых модулей появились такие эффективные средства, как среды программирования, системы автоматизированного проектирования, автоматизированные комплексы управления проектами, са^е-ориентированные инструментальные среды и т.п.. Тенденции создания программного обеспечения ЭВМ свидетельствуют о растущей наукогмкости современных инструментальных систем, т.е. включении в их состав подсистем, основанных на методах теории программирования. Эти методы, направленные на верификацию, оптимизацию и автоматизированное построение программ, являясь довольно сложными в своей математической основе и малоприменимыми непосредственно при проектировании, в то же время могут оказаться весьма эффективными при их использовании в инструментальных средствах программирования.

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

Существенный фундаментальный вклад в этой области научных исследований внесли В.М.Глушков. А.П.Ершов, А.А.Ляпунов, Ю.И.Янов, С.А.Абрамов, Грис Д., Э.Дейкстра., К.Хоар, Дж.А.Бергстра, В.Р.Пратг, Г.Д.Плоткин и др. .

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

за многих проблем, решаемых в настоящее время различными по своим конструктивным особенностям средствами формализации.

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

Объект исследований

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

Цель и задачи работы

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

1. Разработка основных принципов построения максимально унифицированного и простого математического аппарата с хорошими описательными возможностями и пригодного для анализа программного инструментария.

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

3. Проектирование способов эквивалентной трансформации программ с целью их оптимизации и структурирования для сокращения трудоемкости дальнейшей доработки.

4. Разработка способов автоматизации анализа корректности программных систем на основе теории унификации.

5. Применение разработанных средств для исследования и структуризации объектно-ориентированных и интеллектуальных инструментальных классов программ.

Методы исследования

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

Научная новизна

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

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

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

2. Сформулировано понятие концептуальной целостности программного инструментария и предложен конструктивный подход к оценке целостности различных языковых инструментальных средств на основе рассмотрения системы интерпретации языковых конструкций.

3. Доказана эффективность использования теории унификации для проектирования новых методов анализа сложных программ и спроектирован алгоритм частичной унификации термов алгоритмической алгебры. превосходящий существующие алгоритмы по показателю временной сложности.

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

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

6. Конструктивно описано новое понятие сложности программы, основанное на числе возможных трасс ее выполнения. Показано его преимущество в сравнении с аналогичными ранее существовавшими понятиями.

7. На основе свойств гомогенности, полноты, инвариантности и минимальности структур логических моделей предложен подход к структуризации и унификации сложных объектно-орйентировакйых, а также интеллектуальных программных систем.

Практическая ценность' ■■'•' ' "."

Научные результаты, полученные в диссертационной работе позволяют научно обоснованно решать такие практические задачи, как:

- создание концептуально целостных инструментальных языковых средств с повышенными характеристиками надежности,

- разработка наукоемких средств автоматизации проектирования программ со встроенными подсистемами исследования корректности,

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

Достоверность научных положений, выводы и рекомендаций, содержащихся в диссертации подтверждена:

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

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

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

Реализация и внедрение результатов

Результаты диссертационной работы были использованы при разработке автоматизированной информационной системы для исследования рынка интеллектуальной собственности - СИРИС , созданной в рамках научно-технической программы "Интеллектуальная собственность высшей школы" в Научно-информационном центре проблем интеллектуальной собственности при Министерстве общего и профессионального образования Российской Федерации (НИЦПрИС), при разработке системы ведения нормативной документации с возможностью удаленного доступа < 'NormaD-2■■■ в рамках Республиканской научно-технической программы "Информатизация России" в Международной ассоциации информатизации непроизводственной сферы и территориального управления (МАИСТ), при проектировании и реализации автоматизированной системы оперативного управления информационной деятельностью предприятия - <АСОУ ИД (РОСИНФОРМРЕСУРС). В перечисленных автоматизированных программных системах были использованы методологические результаты диссертации в части структурного (регулярного) проектирования и исследования корректности систем.

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

Практическое использование результатов диссертационной работы подтверждено соответствующими документами о внедрении.

Апробация работы

Основные положения и результаты работы докладывались и обсуждались на следующих совещаниях, семинарах и конференциях:

- "Проблемы искусственного интеллекта и распознавания образов", научная конференция с участием ученых из социалистических стран (Киев, 1984г.),

- "Технология разработки экспертных систем", Всесоюзная школа-семинар (Кишинев, 1987 г.),

- "Искусственный интеллект-87", Международная конференция (Suwalky, Польша, 1987г.),

- "Межотраслевая научно-практическая конференция программистов и пользователей ПЭВМ по проблеме защиты информации". (Рязань, 1990),

- "Искусственный интеллект-90", II Всесоюзная конференция (Минск, 1990),

- "/// Всесоюзная конференция по искусственному интеллекту", (Тверь, 1992г.),

- "Международная конференция по информатике", (Рязань, 1993г.),

- "Проблемы математики и информатики", Международная конференция, (Гомель, 1994г.),

- "КИИ-94", IV Национальная конференция с международным участием, (Рыбинск, 1994г.),

- "Научно-технические достижения и интеллектуальная собственность высшей школы". Выставка научно-технических достижений. (Москва, 1994г.),

- "Телематика '95", Всероссийская научно-методическая конференция. (Санкт- Петер б ург. 1995г.), - ■

- "International Conference of Engeneering Education ICEE'95", (Москва, 1995г.),

- "Технологии и системы сбора, обработки и представления информации", международная научно-техническая конференция (Москва. 1995г.),

- "INFOBASE'95", Международная выставка-ярмарка. (Германия, Франкфурт-на-Майне. 1995г.),

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

Публикации

По теме диссертации опубликовано 52 научные работы, в том числе 2 монографии и 2 учебных пособия, получено 6 свидетельств об официальной регистрации программ для ЭВМ.

Структура и объем диссертации

Диссертация состоит из введения, пяти глав, основных результатов, списка литературы и приложений.

Общий объем основного текста включает 285 стр., 23 рисунка, 7 таблиц. Список литературы содержит 210 работ.

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

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

В первой главе приводится краткий обзор научньгл исследований в области формального анализа программных систем. Среди основных направлений этих исследований выделены:

- исследование надежности программ,

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

- исследование корректности автоматизированных систем, в том числе машинными методами,

- разработка средств структурирования и оптимизации программного обеспечения.

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

Чаще всего при исследовании программных систем применяются сразу несколько математических формализмов, один из которых является доминирующим.

Далее в главе рассмотрены результаты, достигнутые до настоящего времени в области формального анализа инструментальных программ с языковой основой. Наиболее известные работы этого направления принадлежат следующим ученым: А.Черчу, В.М.Глушкову, А.П.Ершову,

A.А.Ляпунову, Ю.И.Янову, А.И.Мальцеву, Ч.Хоару, Д.Кнуту. Э.Дейкстре, А.Мили, А.Милнеру, Дж.Бэкусу, И.Винковскому, П.Науру. И.А.Бергстре, М.Балмеру, Г.Плоткину, Р.Барсталлу, С.Гудману, С.А.Абрамову, В.А.Евстигнееву, К.Кнайту, П.Дибье, В.Пратту, М.Фишеру, Г.Бучу, Ф.Бруксу, Р.Андерсену, А.Ахо, Дж.Ульману.

B.Н.Агафонову, Дж.Робинсону и др. Работы этих ученых позволили использовать алгебраические, логические, теоретико-множественные и теоретико-графовые методы для становления принципиально новых технологий программирования и явились фундаментом структурного, объектно-ориентированного и сске-лодходов.

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

В числе недостатков существующих теоретических разработок, препятствующие их широкому практическому внедрению, выделены:

- сложность математических формализмов, требующих от программиста знания многих математических аппаратов,

-возможность внесения ошибок на концептуально-логическом уровне проектирования,

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

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

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

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

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

- упрощение инструментария программирования на основе саве-подхода с целью повышения надежности программ и сокращения трудоемкости их разработки,

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

- построение языка для удобной спецификации программ,

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

- определение признаков структурного проектирования объектно-ориентированных программ, использующих методы унификации,

- разработка эффективных проектных решений, ориентированных на теоретико-унификационные методы.

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

В следующим разделе первой главы дается определение инструментальных программных средств и определяется понятие формальной программной машины (ПМ).

ПМ образует весь набор средств программного инструментария, который содержит в своем составе (рис.1):

- некоторую модель представления данных М, отображаемую на пространство оперативной и внешней памяти ЭВМ,

- константы К, соответствующие модели представления данных,

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

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

- систему управления интерпретацией Ф конструкций ПМ, реализующую базовый алгоритмический формализм языковой системы,

-10- интерпретацию 1 синтаксических конструкций А прикладной составляющей инструментария.

Рис.1. Структурные составляющие инструментария

Полный набор составляющих М, К, А. Ф, Р. I представляет собой формальную ПМ, реализуемую программными средствами алгоритмического языка или другого инструментария.

Формальная ПМ Ть с входным языком Ь представляет собой следующий набор алгебраических систем:

< М, К,, ^ Фь, > .

Алгебраическая система М является алгеброй элементов памяти с определенными на множестве ее элементов отношениями.

Элементы памяти считаются фрагментами оперативной памяти, используемой в конкретном ЯП для множества базовых и производных типов данных, с соответствующими адресами памяти. Так, например, для языков типа Си или Паскаль базовыми элементами М являются адресуемые области памяти, используемые для объектов целого, действительного и символьного типов, из которых синтезируются более сложные производные структуры.

К представляет собой алгебраическую систему констант ЯП. Эта система жестко связана с системой М и соответствует прикладной составляющей модели данных ПМ алгоритмического языка..

Синтаксические конструкции любого из алгоритмических языков содержат управляющие конструкции для организации алгоритмической схемы программы, а также конструкции, используемые для записи операций над базовыми объектами языка. Для исследования этих конструкций в ПМ используются соответственно алгебраические системы F и А. Для универсальных ЯП к системе F относятся такие синтаксические конструкции, как if-then-else, do-while, switch и т.п., система А содержит операции для числовых и строковых типов данных, например +, *, /, = и т.д.

Алгебраические системы Ф и I предназначены для описания интерпретации соответствующих синтаксических конструкций, исследуемых в F и А. Система интерпретации некоторого ЯП представляет собой описание семантики (смысла) его синтаксических конструкций в некоторой более простой системе команд, оперирующей понятиями, заведомо более примитивными, чем понятия этого языка.

Алгебраическая система Ml элементов памяти опре деляется следующей системой множеств:

Ml. = < Am, Qm, Rra >, где пара множеств <Am, Dm > - алгебра элементов памяти, в которой А™

= { mi, ш:..... ш,..... гПп ! - множество адресов базовых и производных

элементов памяти mi, соответствующих определенным типам данных. С1т

- 1 со i.....юк ) - сигнатура алгебры, где о, еП - операции над элементами

памяти для синтеза производных элементов, Rra = {п.....п } - множество

отношений над элементами памяти.

Алгебраическая система констант представляет собой прикладную систему базовых типов данных, используемых в ЯП. Чаще всего эта система рассматривается как многоосновная и включает в себя алгебру символьных строк, алгебру массивов и формальную арифметику.

Алгебра Al, используемая для формального описания в ее рамках синтаксических конструкций языкового инструментария, задействованных в описаниях вычислений над переменными и .константами типов данных, имеет своим носителем цепочки некоторого подъязыка языка L. Они представляют собой простые выражения, не влияющие непосредственно на основной алгоритм программы. В качестве операций используется система подстановок вместо нетерминальных символов цепочек -терминальных литеральных конструкций.

Алгебраическая система управляющих синтаксических конструкций описывает возможные композиции синтаксических конструкций ,ЧП или другого программного инструментария, используемых для записи .структуры алгоритма, и представляет собой следующую систему множеств:

Fi. = <А lib ¿¿т, Rm >',

где пара множеств < Af, > - алгебра управляющих конструкций, в которой Af = { fi.....fi, .., fn } - множество командных конструкций, описываемых порождающей грамматикой Gl некоторого языка L и характеризующих управление вычислениями в программе. Каждая конструкция fi может иметь произвольную местность (fi) = п, говорящую о возможности выполнения п подстановок в те места fi, которые соответствуют нетерминальным символам грамматики Gl. Сами же подстановки являются элементами множества операций Qf, необходимыми для формирования более сложных и более конкретных программ.

Целесообразность формального рассмотрения интерпретации синтаксических конструкций определяется следующими причинами:

1) появляется возможность доказательства правильности композиции различных синтаксических конструкций ЯП в более сложные конструкции:

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

3) строгое рассмотрение интерпретации конструкций приводит к оптимизации алгоритма компиляции программ за счет рассмотрения инъ-ективных отображений синтаксических конструкций в более простую систему операций, а также эквивалентных оптимизирующих преобразований на уровне интерпретирующей системы (программной машины);

4) эквивалентность некоторых сложных синтаксических конструкций может быть доказана через интерпретирующие последовательности.

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

m(xi) - адрес первого элемента объекта (переменной) с именем х,.

m(I,) - адрес операции с именем Ь,

m(Stop) - адрес завершающей выполнение пустой операции,

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

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

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

вания минимальности числа сортов множеств-носителей ПМ при обеспечении полноты функциональных средств инструментария для решения задач, на которые он направлен. Таким образом, чем меньше классов операторных конструкций ЯП, которые необходимо учитывать в композициях при составлении программы, тем более целостен этот язык.

В качестве конкретных примеров использования формализма ПМ в главе приводится исследование программ для языков С и Lisp.

Во второй главе приводится общая постановка проблемы унификации для термов ПМ.

Под унификацией двух термов s и t понимают отыскание таких подстановок на место переменных в обоих термах s и t, которые бы сделали эти термы равными.

Подстановки обозначаются малыми греческими буквами. Пусть подстановка о осуществляет замену в каком-либо терме переменной х, ка терм fi (а, X]), а переменной х2 на терм Ь, тогда это записывается так: о(х,) = fi (a, Xj), c(xz) = b. о = { х, <-fi (a, x¡), xz<-b}.

Применение постановки 0 к терму s обозначается через ст { х, <- fi (а, Xj), xz <- b ¡(s) или сокращенно c(s).

Термы s и t называются унифицируемыми, если существует хотя бы одна постановка о. при которой выполняется равенство cr(s) = a(t); при этом с называют унификатором для s и t, a a(s) - унификагщеи для s и t.

Сложность унификации произвольных термов не только в том, что они могут быть весьма сложными, но и в существовании для всех функциональных символов термов некоторых алгебраических свойств, соответствующих свойствам алгебраических операций, например: А ( ассоциативность ) f(f(xy)z)=f(xf(yz), С ( коммутативность ) f(xy) = f(yx), D (дистрибутивность ) Dr : Г( х g ( у z)) = g ( f ( х у ) f ( х z)),

Di.: f (g (х у ) z) = g ( f ( x z) f (y z)),

H,E(гомоморфизм.

эндоморфизм) (р(х«у) = ф(х)-ср(у),

I (идемпотентность) f(xx) = x,

T (транзитивность ) f(g(xy)g(yz)) = f(g(xy), g(xz)),

Cr.l (левая, правая f(f(xy) z)=f(f(xz)y),

коммутативность ) f(x, f(yz)) = f(y f(xz)).

Особенности алгоритмов унификации для случая термов, описывающих структуру программ в формальных ПМ, позволяют сделать вывод о возможности создания на их основе методов, реализующих следующие функции:

- унификацию функционально-эквивалентных программ или фрагментов программ по программным переменным с помощью замены конкретных имен переменных,

-14- унификацию функционально-эквивалентных программ или их фрагментов с использованием аксиом эквивалентной трансформации (классов эквивалентности);

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

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

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

- доказательство эквивалентности трансформаций программы посредством метода резолюций с эрбрановской базой.

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

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

begin fb(

i:=i+l; Mi),

while x<> 0 do f« (f<>( x, 0 ),

begin fi,(

res[i] := x mod 2; f=(fn(res, i), fm(x,2)),

x := x div 2; f=(x, fd( x,2 )),

i:=i+l; Mi);»

end )

end

Графическое представление терма, соответствующего этому фрагменту программы, приведено на рис.2. При таком представлении появляется возможность использования известных алгоритмов преобразования графов, а также привлечение при конкретной программной реализации алгоритма унификации ЯП, допускающих обработку списков или деревьев (например, соответствующие библиотеки классов С++).

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

Гь

x 0 f= f,- f++

/I Л I

t и frn X f d i

/\ /л^

res i x 2

Рис. 2. Модифицированное представление терма программы

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

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

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

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

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

В главе предлагается новый алгоритм, построенный на следующих принципах. Пусть F - некоторый терм программы, содержащий функциональные символы fi, f;.....fn , символы переменкых xi, хг, ..., xm и символы констант ci, а.....Ck . Тогда дерево, которое соответствует терму F

можно обозначить через Gf: Gf = <->, { fi, f>.....fn , xi, xra , ci, c:,

.... Ck}>-

где —» - отношение подчинения для вершин дерева. л

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

-16Л, Ь, ..., ^ , XI, Х2, ..., Хщ , С!, С2.....Ск

Г1, аи Э|2... аи......... а|т ......... ан;

ана!:... а;п......... а^ш ......... агк

1п , &п1 ап2... апп......... апт ......... а„к

XI, ...........................................................

Х2, ...........................................................

Хт, ат1 Эт2 ... атп......... атт .........атк

С1, ...........................................................

С2. ...........................................................

Ск ак1 акз... аь......... акт ......... акк

Элемент матрицы а^ устанавливается равным 1. если вершины, на пересечении столбца и строки которых стоит этот элемент, связаны ребром дерева вг. и равным нулю в противном случае.

Для упрощения алгоритма доказываются соответствующие теоремы.

Экспериментальная проверка рассмотренных в главе алгоритмов, произведенная на ПЭВМ 1ВМ-486 РХ4 (66 Мгц) на ЯП Си, по усредненным значениям показала следующие показатели временной сложности алгоритмов(рис.3,4).

По вертикальной оси отложены значения времени работы алгоритмов в секундах, по горизонтальной - число связных переменных в обрабатываемых ими термах. График, помеченный кругом, соответствует характеристике модифицированного алгоритма Робинсона, квадратом -модифицированному алгоритму Хьюита. треугольником - предложенному матричному алгоритму. Характеристики, представленные на графике, являются характеристиками реальных программ и поэтому во многом отражают особенности конкретных реализаций. Кроме того, на рисунке представлена характеристика матричного алгоритма, в котором, как и в алгоритмах Робинсона и Хьюита, не использовались эквивалентные трансформации на основе свойств операторов программ.

При использовании эквивалентной трансформации сложность матричного алгоритма практически совпадает со сложностью модифицированного алгоритма Хьюта.

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

Формально функциональное соответствие, которое обеспечивает некоторая программа вей, где Б - некоторое множество однотипных программ с возможными состояниями qí оперативной памяти из пространства состояний С}, можно представить следующим выражением: 5(СЫ = С*,;, или {С2р}з{(Зе}. Под э понимается текст программы на каком-либо ЯП, формальное представление которого описывается ПМ. Тогда б переводит

допуепшые входные состояния q1 е Qp в выходные состояния ЦкеСЬ. Обозначим функциональное соответствие, задаваемое программой, через срф.

Рис.3. Сравнительные характеристики сложности

Рис.4. Характеристики сложности при использовании аксиом Для любой программы s существует некоторый, по-видимому, бесконечный класс эквивалентности Sq, равных ей программ si.s:, ... , отвечающих равенству:

<p(s0 = <p(s2) = ... =<p(s). Отличие этих программ по синтаксической форме обусловливает отличие и по ряду других характеристик. Одной из них является длина терма программы G(s). В качестве другой важнейшей характеристики принято рассматривать эффективность работы программы во времени Ti(s(q,)), являющуюся числом условно принятых тактов ее работы для определенного входного состояния q¡. Идеальной характеристикой эффек-

тивности программы s во времени является среднее арифметическое обработки всех ее допустимых входных данных:

±T(s(q,))

Т0 = —-, где п - число вариантов входных данных.

п

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

Ъм

7 = —-, где п - искусственно ограниченное число трасс про-

п

граммы, a t¡ - время выполнения конкретной трассы. Эту оценку для конкретной программы s будем обозначать через Ts.

Если рассмотреть две программы и sy, для которых справедливо соотношение (cp(s\) = cp(s2) = ... = <p(s)), tp(Sx) = <p(sy), а также s* * sy , то можно сказать, что существует некоторое преобразование p(s4) = Sv, которое переводит синтаксическую форму программы Sv в форму Sv, обеспечивая при этом их функциональную эквивалентность.

Преобразование программ р, такое, что p(sO = sy, называется оптимизирующей эквивалентной трансформацией (оптимизирующим преобразованием) программы S\ в программу sy, если справедливо следующее соотношение: G(Ss) > G(Sy) v T(Sx) > T(s%), где v - символ операции "логическое или".

Абсолютной эквивалентной оптимизирующей трансформацией назовем оптимизирующую эквивалентную трансформацию, для которой справедливо соотношение:

(G(sx) > G(sy) & T(sx) > T(sy)) v ( G(sO > G(s,) & T(s*) >T(Sv)).

Преобразования программ можно выполнять последовательно, одно за другим, например, рх (st) = sy, р> (sv) = s?., и т.д. Если осуществить подстановку py(px(sx)) = sz, то можно говорить о композиции преобразований (р-фу), в которой над программой сначала выполняется преобразование рч, затем ру. В результате такой композиции получается новое преобразование р*у = (рхру), для которого справедливо p<y(sx) = s¿.

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

О = < Р, Q = {°}> , где Р - множество преобразований из S в S ( множество программ ), а Q - сигнатура из единственной операции композиции эквивалентных трансформаций.

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

= - означает отношение функционального равенства элементов, стоящих слева и справа от знака отношения.

s - собственный знак эквивалентности конструкций для аксиом; е - пустой оператор "пропустить";

f= - оператор присваивания (более общее название - оператор изменения значения областей памяти);

f, (...) - некоторый оператор с конечным числом аргументов; заменяет

выражение f, (xi..... хп);

f, (... xi...) - то же самое, но заменяет выражение fi (xi, ..., Xi,... хп) для определения вхождения переменной или оператора в аргумент fi : => - символ следования в аксиоматическом правиле, Т - функция определения эффективности программной конструкции по времени выполнения.

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

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

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

fo - оператор объединения конструкций в единый блок . file - оператор типа if-then-else (условный оператор), fir - сокращенный условный оператор.

Наиболее существенные аксиомы представлены следующим списком.

1) Аксиома пустого присваивания f = (x,x); = е;

2) Аксиома о подстановке

f-Cx.fi (...)): f=(y , i] (... х ...)); = f=(x,U..fiO..) •••));

3) Аксиома о перестановке независимых аргументов

f,(...)±fi (...)=> fi (...); $(...)- f,(...)fi(...) ;

4) Аксиомы определения преобразующих операторов

f=( х, fi (...)) 1 х з false или —. f=( х, fi (...)) -L х;

5) Аксиомы временного предпочтения

f. (-. fo ...) = fj (... f> ...) & T(f, (... f0 ...))> T(fj (... f, .. •));

6) Аксиома повторного изменения элемента памяти Vf,-,arg(fj. х) & 3!х (-, f, 1 х) => fi(... х ...); ... x ...); a fj(... x ...);

7) Аксиома об исключении неизменяемых и неизмепяющих обл астей памяти VR Эх arg(fj, fi) & Зх —.arg(fj, х) & (ii 1 х ) => fi(... х ..) = е ;

-208) Аксиома о блокировании аргументов

fxl fy & fx = fy & -iFunc(fx)& -iFunc(fv) => ' fx(fi): fy(fj)sf,(f«(fi ;fj ));

9) Аксиома об эксплантации инвариантных аргументов

fx-Lfy => fx(... fy... ) = fy; fx (••• e...);

10) Аксиома об условном операторе:

f= (xi, false); fife(x,, xj: Xk) = f=(x, false); Xk .

11) Аксиома о сокращении условного оператора:

f=(xi, false); fr (x,, xk) = xk.

12) Аксиома исключения единичного оператора:

fi(...);e; = e;fi (...); = f, (...).

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

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

Регулярные структуры программ - это схемы алгоритмов программ, подчиняющиеся строго очерченному множеству правил, дающих возможность получения положительного эффекта при их применении в разработке и преобразовании программных систем. Для конструктивного определения таких структур доказаны теоремы.

Теорема

Для двух интерпретирующих последовательностей (дизъюнктов) On и Фу, все элементы которых находятся в отношении функциональной независимости, перестановка последовательностей Фх • Фу = Фу • Фх сохраняет эквивалентность соответствующих им трасс выполнения программы.

Теорема

Если в трассе выполнения программы существует интерпретирующая последовательность <р-, • Ov • щ такая, что элемент фу является обратным элементу фх и элементы <рк и <ру попарно независимы от каждого из элементов Ф( , то является справедливым следующее соотношение: фх • Ф1

• фу = 01 .

Следствие Если справедливо соотношение фх • Ф( -фу = Фс, для обратных друг другу элементов срх и фу , то независимость фх и Ф1 предопределяет и независимость % от Ф(.

Теорема

Если в трассе выполнения программы существует интерпретирующая последовательность <рх • Ф( -фу такая, что элементы интерпретации фч и

Фу являются обратными условными интерпретациями, и фх-i функционально независим от каждого из элементов <i>t, то эта трасса эквивалентна нулевому элементу <pj_(e. Stop).

Далее показывается, что независимо от ЯП можно выделить в нем программы регулярной структуры. Они должны отвечать требованию представимости в форме терма алгебр ПМ с минимальным числом операций композиции фрагментов программ, свойства которых допускают эквивалентную трансформацию в дизъюнктивную нормальную форму (ДНФ) термов, являющуюся развернутой записью возможных трасс выполнения программы.

На основе полученного конструктивного описания регулярных структур программ исследуется система структурных операторов Э.Дейкстры, показывается ее неполнота для выделения регулярных программ, и вводятся новые операторы do-back и deadend, приводящие к полноте дейкстровской системы.

В третьей главе в достаточно общем виде приводится формализация проблемы исследования корректности программ в рамках конкретной ПМ.

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

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

- область определения программы Dom(s),

- область значений Ran(s),

- соответствующее программе функциональное отображение fs.

Спецификацию программы s будем называть полной по областям определения и значений, если для каждого оператора Si этой программы абсолютно точно заданы соответствующие множества Dorn(sO и Ran(s,). Под абсолютной точностью здесь понимается несуществование какого-либо элемента памяти, который бы входил в множества Dom(Si), Ran(Si) и не был бы определен спецификациями для si , и наоборот, невозможно существование элемента памяти, отвечающего спецификациям s, и не принадлежащего Dom(s,) и Ran(Si).

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

Теорема

Множество М| элементов памяти, являющееся областью определения или областью значений некоторого фрагмента программы б, пред-ставимо в виде выражения

М| = Моо'п Мо| П ... пМоп и ... и МшОПМш! П ... П Мгап, где аргументами его правой части являются множества, определенные выражениями спецификации для простейших операторов.

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

Теорема',

Для множеств элементов памяти, представляющих собой области определения и значений некоторой программы 5, можно всегда найти представление в виде выражения

М| = Мо иМ|и... иМ,и...и Мш, где каждому М, будет соответствовать единственный дизъюнкт выражения ДНФ для программы з.

Теорема

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

Одним из интересных случаев сопоставления структур программ с целью поиска родовидовых отношений как внутри ее фрагментов, так и между различными программами, является использование в программных термах переменных. В этом случае появляется возможность использовать каркасный подход. При этом алгоритм унификации программных термов Эх и Бу решает задачу составления решаемого уравнения вида 5* + бу = Бх при помощи подбора соответствующих переменных. Используя представление термов в ДНФ, можно найти алгоритмы унификации, составляющие более сложные уравнения, например: е.* + = е, где е - единичный оператор, а "+" - операции композиции программ.

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

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

нения, и соответствующую числу дизъюнктов ДНФ этого терма, обозначим через C(s\) и C(sy). При параллельной композиции термов получается результирующий терм s*y = s* + sy . Поскольку такая композиция при рассмотрении программ в ДНФ означает приписывание дизъюнктов терма Sy к дизъюнктам терма sx, то сложность результирующего терма будет оценена суммой:

Cv(s,y) = С (s.,) + С (Sy ) . Эта сумма оценивает общую сложность результирующей программы, если в ней нет совпадающих трасс, т.е. для St + Sy не производится никакой оптимизации.

Расчет сложности для архитектур, построенных на основе последовательной композиции s4\ = Sx 0 Sv, выглядит так: _ U:(sJ + C(sJ,ps^ epSp,

L. ( S sv ) — <

[rCïJxOy./M, epS„.

где psi - позиция оператора s, , в которую необходимо подставить оператор. a pSP - множество позиций, являющихся альтернативными другим элементам оператора. pSn - множество позиций, являющихся последовательными другим элементам оператора.

Относительная простота представления выражений для сложностей программных архитектур позволяет анализировать изменение сложности при трансформации программы или сопоставлении эффективности архитектур, получение которых возможно в конкретной ПМ.

В четвертой главе рассматривается использование формализма ПМ для анализа объектно-ориентированных систем. Для этого формализации подвергаются понятия программных объектов и классов.

Пусть задана ПМ и некоторая составленная в ее рамках программа s. Каждый элемент памяти m, е Mi. в этой программе выделяет некоторое подмножество F, с Fl операторов, для которых справедливо утверждение:

fx e F,, m, е Dom( fx ) v m, e Ran( f* ), т.е. этот элемент памяти либо входит в область определения операторов из F,, либо входит в их область значений. В программе s можно выделить некоторую пару множеств ( Мп, F, ), элементы которых функционально связаны между собой. Добавив множество констант К, ç Kl. которые могут означивать элементы памяти из Мн, можно получить новую систему множеств:

Qi = M Fi х Ki, С, = < Qi, Fi > .

Система С, представляет собой некоторую "капсулу", содержащую только те элементы памяти и те операторы, которые определяют изменение состояния памяти, описывающейся множеством Mfi - Систему Ci называют объектом программы. В этом случае система Ci = < Qi , F, > будет представлять собой алгебру, носителем которой являются состояния

оперативной памяти, а сигнатурой - множество операторов или функций изменения состояний памяти.

Для формального описания классов необходимо воспользоваться понятием множества имен элементов памяти. Обозначим это множество через N (МО, где М, - множество элементов памяти. Если в систему С, вместо подставить это множество имен, то будет получена новая система С1а5$1=< Ы(М;), Р(>, которая и соответствует понятию класса.

Для представления смены состояний объекта можно использовать графическое представление (рис.5). Такое представление состояний является графом Ох=<(2х,-» изменения состояний. Его вершинами являются конкретные состояния объекта из множества возможных состояний СЬ. а ориентированными ребрами - отношения следования по ходу выполнения программы.

q2 4з Я-» 45 Чч

Граф изменения может находится в регулярной форме, если он представим алгебраическим выражением с использованием операций последовательной и параллельной композиции, фигурных скобок для представления его циклических фрагментов и круглых скобок для задания приоритета операций композиции. На рисунке 5 представлен регулярный граф изменения состояний. Для него можно составить следующее алгебраическое выражение:

С.х = ((41, 42) • (42, 43) • ( Ч-», 45) + (я*) • (46. 47) • { ( 46. Я7) • (47, 48 ) ■ (48. 4<0 } ) ■ (45 • 49), где "•" - операция последовательной композиции ребер графа ( как переходов из состояние в состояние ), а "+" - параллельная композиция. В фигурные скобки заключена петля, образованная цикличностью изменения состояний.

Операции над классами относятся к алгебраической системе классов, множеством-носителем которой являются классы С, которые можно построить в конкретной ПМ. В качестве основного множества отношений К = {<-», —>, е}, используются бинарные отношения: функциональной зависимости, "1"- функциональной независимости, "->■"- наследования, "с"- включения.

Основными операциями Q = { ©. ® }ная классами являются операции: Ф - сопоставления классов, ® - объединения классов .

Для двух классов операция сопоставления приводит к появлению нового класса, более общего, чем классы, стоящие в аргументах операции. Наиболее частым результатом этой операции является Null-класс: < N(0), 0>. Использование этой операции позволяет организовать иерархию классов или исследовать их декомпозицию. Операция объединения классов заключается в соответствующем теоретико-множественном объединении элементов данных и методов класса соответственно: Clacc* = Class* ® Cfc^ : Class* = < N(MX), Fx >, Classv = < N(My), Fy > Class, = < N(Mt), Fz >, N(M?) = N(Mx) u N(My), Fz = Fx u Fv. Эта операция важна для исследования свойств классов и, в частности. их декомпозиций. Далее приводятся основные свойства операций, полезные при исследовании объектно-ориентированных ПМ.

1) Коммутативность операции сопоставления.

Для двух объектов X и Y справедливо соотношение X ® Y = Y ® X.

2) Коммутативность операции объединения.

Для двух объектов X и Y справедливо соотношение X ®Y = Y ® X.

3) Ассоциативность операции сопоставления. Для трех объектов X . Y и Z справедливо соотношение:

X©(Y©Z) = (X©Y)©Z = X®Y®Z.

4) Ассоциативность операции объединения.

Для трех объектов X , Y и Z справедливо соотношение: X®(Y®Z) = (X®Y) ®Z = X®Y®Z.

5) Для большинства ПМ выполняется также свойство левой и правой дистрибутивности операции сопоставления относительно операции объединения:

X © ( Y <8> Z) = X ® Y ® X Ф Z , ( Y ® Z) © X = Y © X ® Z © X . Далее в главе на основе понятия объектно-ориентированных ПМ рассматриваются полезные алгебраические свойства классов, объектов и состояний объектов. Среди свойств классов выделяются оптимизирующие преобразования. Исследование этих свойств становится возможным в результате использования следующих доказанных теорем. Теорема

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

Теорема

Существует взаимооднозначное отображение (изоморфизм соответствующих алгебр) с точностью до функциональной эквивалентности состояний между операцией параллельной композиции ребер графа G изменения состояний объекта С и операцией параллельной композиции операторов одного из методов класса Class полнообъектной программы, которому принадлежит объект С.

Следствие

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

К оптимизирующим преобразованиям относятся:

- устранение состояний-посредников для группы объектов.

- преобразование транзитивных замыканий,

- устранение функционально-эквивалентных состояний,

- использование свойств дистрибутивности.

В заключительной части главы рассматривается структурный подход к объектно-ориентированному проектированию. Главными критериями структурных программ являются:

- полпота отражения в логической модели предметной области наибольшего числа элементов, подразделяемых на объекты и отношения:

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

- инвариантность свойств структуры, т.е. сохранение ее свойств при внесении или удалении новых объектов и отношений;

- минимальность базиса отношений, на основе которых порождаются производные объекты и отношения.

В объектных программах выделяются типы нерегулярных структур и приводятся конструктивные методы их редукции к функционально-эквивалентным регулярным структурам.

В главе приводятся примеры для ЯП CLOS и С++.

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

Каждая из особенностей определенным образом влияет на формализм ПМ, в рамках которого можно исследовать интеллектуальные программы. Выделим явно те изменения, которым должен быть подвергнут этот формализм:

- необходимо использование множественных значений констант для элементов памяти,

- способы соотнесения значений элементам памяти должны опираться на нечеткие меры соответствия,

-27- необходимо отражение изменения программных термов в конструкциях самих термов, т.е. использование переменных, определенных на множестве программных подтермов,

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

- необходимы формальные средства для исследования вариантов работы программы с одним и тем же набором входных данных.

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

- продукционные системы,

- системы эвристического программирования,

- программы логического проектирования,

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

- естественно-языковые системы.

Пусть левые и правые части правил некоторой продукционной системы определены на множестве некоторых элементов памяти, например, слотов для фреймового представления. Обозначим это множество через А = { а|.....а„ ¡. Как и для других алгебраических систем элементов памяти. для множества А можно определить операцию композиции "+". которая позволяет объединить несколько элементов данных в единый элемент для идентификации его как точной области определения или значений для некоторого продукционного правила. Таким образом, задана алгебраическая система элементов памяти А = < А, { + , Я > . Алгебра управляющих синтаксических конструкций Р = < И, {*, + },#> относится к классу решеток и позволяет рассматривать любые параллельные и последовательные композиции правил. При этом связь алгебр А и Р заключается в том, что все термы из И имеют своими аргументами только элементы множества А.

Далее рассматриваются примеры повышения эффективности продукционных программ для ЯП 01Жи.

В качестве системы множеств, направленной на исследование инструментария эвристических программ, предлагается алгебраическая система с метауровнем или мгтаалгебрапческая система'.

П = < С>, Б, Н, Я >, в которой множества <3, Б и Я аналогичны соответствующим множествам алгебры изменения состояний, а множество Н представляет собой множество операций, определенных на множестве Б.

Рассмотрим множество Н = { 1и, ..., Ьп }. Его можно разделить на два подмножества, в одном из которых будут присутствовать операции обобщения элементов из Б и <3, а во втором - операции последовательной и альтернативной композиции элементов Б.

Для построения планов решения задачи можно использовать точное условие определения отношения род-вид, которое может учитывать ранг отношения:

IsA ( qa, q<j) & IsA(qc, qr) & 3 qr, qt, IsA (qa, qr) , IsA( qr, qa ), IsA(qc, qt), lsA( qu qr) & 3 Sx e S, s* (qa, qc) => В sy e S, sy (qa, qf) & IsA (Sy, sx) -Для интеллектуальных систем, основанных на алгоритмах сопоставления, родовидовые отношения, как отношения над фреймами, являются центральной составляющей ПМ.

Если рассмотреть фрейм как элемент памяти некоторой формальной ПМ, его можно представить следующей конструкцией: N: IsA( N,pN), fa(x,,x:.....х„);

fb ( Xr, Xr+I, ..., Xt ).....fc ( Xh, Xh+l.....Xm ) ,

где N - имя фрейма, pN - имя родовидового предка фрейма, связанного с ним соответствующим отношением, а Га, fv>.....fc - слоты фрейма, представляющие собой некоторые списки характеристик с возможными значениями, представленными собственными аргументами.

Пусть в алгебре синтаксических конструкций фреймового инструментария существует множество-носитель, представляющее собой множество возможных фреймов F = { fi.....f„ }. Две операции { * , + } предназначены соответственно для формирования фреймов-наследников и независимых напрямую фреймов программы. Каждый фрейм f, может содержать некоторое число m слотов. Будем обозначать это следующим образом: fi ( xi, ..., xm ). В этих обозначениях можно описать смысл предложенных операций:

fa ( Xla, ..., Xraa ) + fb ( Xlb.....Xkb ) = fa ( Xla..... Xma ) + flb ( X|b.....Xkb )l

fa ( Xla.....Xma ) * fb ( Xlb.....Xkb ) = fc( Xic, .... Xhc ) +

fap ( Xlap, ..., Xmap ) + fbp ( Xlbp.....Xkbp ),

где ";" - синтаксическая конструкция разделения фреймов (разделитель), а

fc(xic..... Хне ) - фрейм, полученный в результате пересечения множеств

СЛОТОВ фреймов fa ( Xla, ..., Xma ) И fb (Xlb..... Xkb ), фреЙМЫ fap ( Xlap.....Xmjp )

и fbp ( xibp,..., Xkbp) представляют собой преобразованные фреймы fa ( xia,

..., Xma) и fi, ( xib.....Хкь) путем удаления из них общих слотов.

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

В заключительной части главы рассмотрены системы естественноязыкового общения с приведением примеров на ЯП ATN.

В приложениях рассматриваются конкретные программные системы, реализованные и внедренные автором с использованием научных резуль-

татов диссертации, приведены документы, подтверждающие внедрение. Обобщенные архитектуры систем приведены на рис.6-9 (Приложение).

Основные результаты работы

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

2. Сформулировано понятие концептуальной целостности и определен конструктивный подход к оценке целостности различных языковых инструментальных средств. Рассмотрены программные машины современных языков программирования С и Lisp. Разработана концепция формального анализа этих языков'. Описан способ анализа инструментальных программных средств при помощи системы интерпретации языковых конструкций.

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

4. Произведена аксиоматизация правил эквивалентной тран сформации алгоритмов, доказана ее эффективность в сравнении с существующими правилами оптимизации программ. На основе использования графов трасс выполнения программ разработан метод анализа информационных зависимостей для вычисления предикатов функциональных связей. Доказаны теоремы о функциональной независимости интервалов графа трасс. Определены регулярные структуры программ для алгоритмических инструментальных и языковых средств различных классов. На основе алгебраического исследования регулярных структур программ показана их эффективность для оптимизации программ и совершенствования инструментальных и языковых программных средств.

5. Конструктивно описано новое понятие сложности программы, основанное на числе возможных трасс ее выполнения. Показано его преимущество в сравнении с аналогичными ранее существовавшими' понятиями. Разработан метод стратифицированной спецификации, да;ощий возможность описания спецификации и эффективного исследования корректности сложных программных систем. .

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

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

8. Определены особенности формального анализа и оптимизации продукционных программных систем. Рассмотрена классификация продукций, а также основные конструктивные признаки классификации, позволяющие выделять КНФ продукционной программы, используемую при доказательстве ее корректности и оптимизации. Показано эффективное использование формализма ПМ для анализа эвристических программ. используемых в интеллектуальных решателях задач. Определено понятие метаалгебраической системы, позволяющее производить анализ сложных эвристических программ. На основе описания родовидового отношения в эвристических программах приведен обобщенный алгоритм конструктивного формирования решения эвристических задач. Введено понятие нормализованной фреймовой структуры, являющееся одним из эффективных средств исследования корректности и оптимизации интеллектуальных программ, ориентированных на алгоритмы унификации и сопоставления. Показана эффективность использования модифицированных ПМ для анализа большого класса интеллектуальных систем, включающих эвристическую составляющую.

Основные результаты диссертации опубликованы в следующих работах и свидетельствах о регистрации программ.

МОНОГРАФИИ

1. Каширин И.Ю. Объектно-ориентированное проектирование программ в среде С++. Вопросы практики и теории. М.: Госкомвуз России, "НИЦПрИС", 1996. - 192с.

2. Каширин И.Ю., Коричнев Л.П. Формальное исследование интеллектуальных программных систем. - М.: Радио и связь, 1997. - 160с.

УЧЕБНЫЕ ПОСОБИЯ

3. Каширин И.Ю.. Новичков B.C., Потапов В.М. Разработка программ на языке С. - М.: Госкомвуз России, "НИЦПрИС", 1996. - 132 с.

4. Каширин И.Ю. Теория алгоритмов и формализация исследования программ. - Рязан. гос. радиотехн. акад., Рязань, 1996. - 80с.

СТАТЬИ И ДРУГИЕ ПУБЛИКАЦИИ

5. Каширин И.Ю. Алгебраический подход к исследованию программного инструментария сетей ЭВМ //Электросвязь. -1996.-N- с.14-17.

6. Kashirin I.Yu. An Algebraic Approach to Object-Oriented Systems Design // Intern. Confer. "Problems of Mathematic and Informatic", HGU, Hornel, 1994, - c.47.

7. Kashirin I.Yu., Korichnev L.P. The Use of Program Semantic for Unifiable Object Representation in Object-Oriented Design. - Intern. Conf. of Math. & Inf. Probl. , HGU, Hornel, 1994. - pp. 12-14.

8. Каширин И.Ю. Оптимизация сетевых протоколов с использованием унификации. - Электросвязь, N2, 1997. - с.29-32.

9. Каширин И.Ю. Алгебраическое исследование расширенных сетей переходов для проектирования лингвистических процессоров. // В кн.: Программное обеспечение сложных автоматизированных систем.-М.: ВЦ АН СССР, 1988,- с.З - 12.

10. Каширин И.Ю. Исследование частичной корректности программ. - Инф. бюлл. "Интеллектуальная собственность высшей школы", N7, 1996. -C.97-109.

11. Каширин И.Ю. Алгоритмические алгебры: формальный подход к проектированию лингвистических процессоров. / Межвуз. сб. научных трудов "Техническое и алгоритмическое обеспечение информационно-преобразовательных систем", Рязань, РРТИ, 1986. - c.5;lQ,,

12. Каширин И.Ю. Подсистема естественно-языкового общения конечного пользователя с типовой АСУ МТС с/х. - Материалы Всесоюзной НТК "Проблемы производственно-технического обеспечения с/х в условиях агропромышленного комплекса, Рязань, ВНИИМС, 1984. -с. 127-130.

1 З.Алешин А.Ю.,Каширин И.Ю.,Шерстнев В.Ю.,Щенников С.Ю. Средства интеллектуального взаимодействия с типовыми АСУ. / Межвуз.

сб. "Системы управления, сбора и передачи информации", Рязань, РРТИ, 1985. - с.24-29.

14. Гаврюшин А.Д.,Каширин И.Ю. Адаптивный подход к проектированию моделей диалога и языка в системе естественно-языкового общения. - В сб. "Совершенствование МТС агропромышленного комплекса на основе ускорения НТП", Рязань, ВНИИМС, 1986. - с.100-106.

15. Каширин И.Ю..Романов В.М. Автоматизированная система оперативного управления деятельностью предприятия (организации). -ИЛ, Рязань, ЦНТИ, 1989. - 2с.

16. Каширин И.Ю. Защита знаний в интеллектуальных системах. -Доклады межотраслевой научно-практической конференции программистов и пользователей ПЭВМ по проблеме защиты информации, Рязань, ЦНТИ, 1990. - с.14-15.

17. Каширин И.Ю.,Линькова C.B. Принципы проектирования системы оперирования знаниями в системе программирования ATNL/2./ Межвуз.сб. "Программные средства и устройства информационных и преобразовательных систем", Рязань, РРТИ, 1991. - с. 19-25.

18. Kashirin I.Yu. Khoroshevsky V.F. ATN-oriented linguistic processors design (An algebraic approach). - Intern. Conf. Artificial Intelligence-Suwalki, Poland, 1987. -c.74.

19. Каширин И.Ю., Николов B.C., Щенников С.Ю. Проектирование компонент экспертных систем в инструментальной среде "ПИЭС". -Доклады республиканской школы-семанара "Технология разработки экспертных систем", Кишинев, САИИ. 1987. -с.76-80.

20.Каширин И.Ю. Конструкции языков программирования. Математическая формализация. - Труды международного научно-технического семинара "Проблемы передачи и обработки информации в информационно-вычислительный сетях", Москва, МАИ, 1995.-с.46-49.

21.Каширин И.Ю. Унификация в системах описания семантических представлений. / Межвуз. Сб. Научных трудов "Элементы, устройства и программные средства информационно-преобразовательных систем", Рязань, РРТИ, 1989. -с.14-17.

' 22.Каширин И.Ю. ATNL/2 - язык программирования общения с интеллектуальными системами. - II Всесоюзная конференция "Искусственный интеллект-90", Минск, САИИ, 1990. - с.22-26.

23.Каширин И.Ю.,Коричнев Л.П. Проектирование распределенной информационной системы с интеллектуальной поддержкой. - Труды Всероссийской научно-методической конференции "Телематика'95", Санкт-Петербург, 1995. - с.64-65.

24.Каширин И.Ю., Хорошевский В.Ф. Конструирование диалоговых систем с фрейм-ориентированным представлением проблемных знаний на основе ATN-формализма.-Научная конференция с участием ученых из социалистических стран "Проблемы искусственного интеллекта и распознавания образов", Киев.ИК АН УССР,ВЦ АН СССР,1984.-с.86-89.

-3325. Каширин И.Ю. Программное обеспечение учебных курсов направления "Искусственный интеллект" .-Сб. трудов научно-методической конференции преподавателей, Рязань, РРТИ. 1993. - с.33-35.

26.Каширин И.Ю. Согласование и унификация знаний на основе понятийных дихотомических базисов. / Международная конференция "Технологии и системы сбора, обработки и представления информации", Рязань, МАИ, 1993. с. 67-68.

27.Каширин И.Ю. Семиотическая модель в естественно-языковой системе, ориентированной на знания. / Межвуз. сб. "Элементы, устройства и математическое обеспечение информационно-преобразовательных систем", Рязань, РРТИ, 1985. - с.5-9.

28.Каширин И.Ю. Критерии семантической адекватности представления знаний в языковых моделях. I Межвуз. сб. "Обработка' и передача данных в информационно-вычислительных сетях", Рязань, РРТИ, 1992. - с. 14-17.

29.Каширин И.Ю.. Коричнев Л.П., Новичков B.C. Подход к формальному исследованию объектно-ориентированных программ. / Межвуз. сб. "Информационные технологии. Системы обработки и передачи информации", Рязань, РГРТА, 1996. - с.33-39.

30.Каширин И.Ю., Коричнев Л.П. Методы формального анализа сложных программных систем. / Сб. научных трудов "100 лет радио", Рязань, РГРТА, 1995. - с. 96-100.

31.Каширин И.Ю.. Коричнев Л.П., Потапов В.М. Автоматизированный информационный комплекс для исследования проблем интеллектуальной собственности. I Труды информационного форума информатизации, Москва, 1995. - с. 9-10.

32.Каширин И.Ю.. Коричнев Л.П. Распределенная информационная система для исследования рынка интеллектуальной собственности. /Межвуз.сб. "Математическое и программное обеспечение информационных и управляющих систем", Рязань, РГРТА. 1995. с. 7-13.

33.Каширин И.Ю. Исследование абстрактных типов данных в конструкциях современных алгоритмических языков. ! Труды международной конференции "Технологии и системы сбора, обработки и представления информации", Москва, 1995. - с.28-29.

34.Берзин Б.П.,Дедковский В.П..Каширин И.Ю..В.М.Романов Перспективы использования ПЭВМ в информационней деятельности территориальных органов НТИ. / Научно-технический сборник "Информационная деятельность территориальных органов НТИ", Вып.З, Москва, МГЦНТИ, 1990. - с. 12-17.

35.Каширин И.Ю. Принципы регуляризации программных модулей логического уровня для объектно-ориентированного проектирования. / Межвуз. сб. "Математическое и программное обеспечение информационных и управляющих систем", Рязань, РГРТА; 1995. - с.82-90.

36.Каширин И.Ю. Инструментальная среда для проектирования интеллектуального интерфейса. / Сб. научных трудов IV Национальной конференции с международным участием "Искусственный интеллект -94", Рыбинск, КИИ, 1994. -с.360-363.

37.Kashirin I.Yu., Korichnev L.P.,Potapov V.M. An lntegrated-certificated environment. Quality, Economy, Possibilities. - International conference of engineering education, ICEE'95, Moscow, Russia, 1995. - p. 123.

38.Каширин И.Ю.,Коричнев Л.П. Система автоматизированного формирования синтаксических анализаторов фразеологии деловых текстов. - Труды VII научно-методической конференции "Методы обучения и организация учебного процесса в вузе", Рязань, РГРТА, 1995. - с.52-55.

39.3юрина Г.В.,Каширин И.Ю.,Потапов В.М. Распределенная информационная система для автоматизации исследования рынка интеллектуальной собственности. / Инф.бюлл. "Интеллектуальная собственность высшей школы, N6, 1996. - с.8-11.

40.3юрина Г.В.,Каширин И.Ю. Информационная фактографическая система Infond v.l.12 ведения нормативной документации по интеллектуальной собственности под управлением MS Windows. - Каталог выставки "Научно-технические достижения и интеллектуальная собственность высшей школы. Раздел "Программный продукт и базы данных"", Москва, 1994, с.7.

41.3юрина Г.В.,Каширин И.Ю. Автоматизированная система для поддержки работ по исследованию рынка интеллектуальной собственности в регионах Российской Федерации. - Каталог выставки "Научно-технические достижения и интеллектуальная собственность высшей школы. Раздел "Программный продукт и базы данных"", Москва, 1994, с.8.

42. Каширин И.Ю. Задачи и функции унификации для формальных структур программ. - Сб. трудов "Управление образовательным процессом в высших учебных заведениях", Рязань, РГРТА, РВВКУС. 1997. -с.16-19.

43. Каширин И.Ю. Проектирование общения с прикладными программами в системе Scate/ATN. - Сб. научных трудов III Конференции по искусственному интеллекту КИИ-92. Тверь, АИИ, 1992, е.- 117-119.

44. Каширин И.Ю. Теоретико-множественный подход к спецификации программ, использующих базы данных. - Инф. бюлл. "Интеллектуальная собственность высшей школы", N7, 1996. -с.53-61.

45. Каширин И.Ю. Формальное исследование интеллектуальных инструментальных программных систем. I Межвуз.сб. "Информационные технологии. Системы обработки и передачи информации" , Рязань, РГРТА, 1996. - с.39-48.

46.Каширин И.Ю. Исследование программных систем унифика-ционными методами. / Всероссийская научно-практическая конференция "Современные информационные технологии в образовании", Москва. 1996. с. 15-17.

АЛГОРИТМЫ И ПРОГРАММЫ

47.Каширин И.Ю. и др. Комплекс программных средств автоматизации системы регистрации программ для ЭВМ (HD v.l.Ol) I Свидетельство об официальной регистрации программы для ЭВМ, РосАПО, N 940317.

48.Каширин И:Ю. и др. Электронная почта для MS Windows (R&S Mail v.1.1) / Свидетельство об официальной регистрации программы для ЭВМ, РосАПО, N 940316.

49.Каширин И.Ю. и др. Инструментальная среда формирования сдоварно-понятийной базы (VCreate v.2,01) I Свидетельство об официальной регистрации программы для ЭВМ, РосАПО, N 940303.

50.Каширин И.Ю. и др. Автоматизированная информационная система для исследования рынка интеллектуальной собственности. / Свидетельство об официальной регистрации программы для ЭВМ, РосАПО, N 950484.

51. Каширин И.Ю. Программа ретрансляции и оптимизации логических алгоритмов / Свидетельство об официальной регистрации программы для ЭВМ, РосАПО. N 960037.

52. Каширин И.Ю. Транслятор с языка программирования Scate (Scate - транслятор) / Свидетельство об официальной регистрации программы для ЭВМ. РосАПО, N 970063.

-36-

ПРИЛОЖЕНИЕ

Исчоцшс. тексты

С насм.ч

ФчПЛСр

Рел:иаор

Лексические таблицы

.. ..„.

ГГп

рсер

« у 1 г

... ,......

Таблицы схем

Таблицы правил

Таблицы фактов

Ошимйллор

Гоювыс.

опмдчйк

Рис. 6 Архитектура среды языка программирования Scate Среда Scate/ATN представляет собой систему программирования ориентированную на разработку интеллектуальных систем с естественноязыковым интерфейсом и возможностью логического вывода.

Среда состоит из двух относительно независимых друг от друга инструментальных языковых подсистем: языка программирования логического типа Scate и сетевого языка ATN.

Требования к ПЭВМ: Совместимость с IBM-PC/XT/AT, объем оперативной памяти не менее 1 Мбайт, объем накопителя на жестких мег-нитных дисках не менее 20 Мбайт. Требования к операционной системе: версии MS/DOC v.6.00 и поздние, совместимые с ней.

ш 1 Л

Администрация города

Modem

ВНЕШНИЙ !

ИНТЕРФЕЙС С I

ДРУГИМИ ;

СИСТЕМАМИ :

Экологическая система

Ц в д

ТЕЛЕФОН

ПОДСИСТЕМА В Е Д Е H ИЯ ДОКУМЕНТАЦИИ

Server IBM

compatible

5Ü3

Workstation *нлг*сн

• • •

объекты управления города

ИСТОЧНИКИ ИНФОРМАЦИИ

Рис.7 Информационная система управления развитием города

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

Рис. 8

На рис.8 приведена архитектура автоматизированной информационной системы, предназначенной для исследования рынка интеллектуальной собственности в современных экономических условиях России.

БД

Подсистема архивирования

Подсистема оперативного контроля

Документы

Массив НМД

Расчет экономических показателей

Планово-экономические органы

□ О

||Т»п1П1П11чщццтщ

Раб. место

Раб место

.Printer

Администрация предприятия

Потребители продукции

Рис.9 Автоматизированная система управления предприятием

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