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

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

БУТАКОВ МИХАИЛ ИГОРЕВИЧ

ИНСТРУМЕНТАЛЬНОЕ СРЕДСТВО СИНТЕЗА И ИСПОЛНЕНИЯ ТРАНСЛИРУЮЩИХ ПРОГРАММ НА ОСНОВЕ ПОЗИТИВНО-ОБРАЗОВАННЫХ ФОРМУЛ

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

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

1 МАР 2012

Иркутск-2012

005010812

Работа выполнена в Учреждении Российской академии наук Институте динамики систем и теории управления Сибирского отделения Российской академии наук (ИДСТУ СО РАН).

кандидат физико-математических наук, доцент

Курганский Виктор Иванович

доктор физико-математических наук, профессор

Маицивода Андрей Валерьевич

кандидат технических наук Черкашин Евгений Александрович

Институт проблем управления им. В.А. Трапезникова РАН (г. Москва)

Защита состоится 15 марта 2012 г. в 14:00 на заседании диссертационного совета Д 003.021.01 в ИДСТУ СО РАН по адресу: 664033, г. Иркутск, ул. Лермонтова, 134.

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

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

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

С диссертацией можно ознакомиться в библиотеке и на официальном сайте www.idstu.irk.ru ИДСТУ СО РАН.

Автореферат разослан 14 февраля 2012 г.

Ученый секретарь диссертационного совета д.ф.-м.н.

А.А. Щеглова

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

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

Актуальность темы исследования. Для расширения функциональных возможностей современных прикладных программ часто приходится решать задачи трансляции: макроязык VBA в Microsoft Office, макроязык AutoLisp в AutoCad, предметно-ориентированный язык 1С: Предприятие в продуктах 1С и др.

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

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

• адаптировать средства интеллектуализации к терминологии и свойствам предметной области;

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

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

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

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

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

Большая часть работы основана на результатах, полученных С.Н. Васильевым и его учениками в области логического вывода и приложений логического вывода в составе пакетов прикладных программ. Предпосылкой для исследования послужили работы Ершова А.П. по доказательному программированию. При решении части задач были использованы идеи дедуктивного и структурного синтеза программ, изложенные в работах 3. Манна, Р. Уолдингера и Э.Х. Тыугу. Существенное влияние на результаты диссертации оказали работы Н. Хомского, А. Ахо и Дж. Ульмана, посвященные моделям и методам трансляции.

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

Цель и задачи исследования. Цель работы - на основе ПОФ разработать инструментальное средство конструирования и применения транслирующих программ в составе прикладных программ для формальных языков второго и третьего классов по Хомскому.

Для достижения указанной цели были решены следующие задачи:

1. Разработать постановку и схему решения задачи трансляции в исчислении ПОФ;

2. Разработать алгоритмы построения распознающих ПОФ по регулярной правосторонней детерминированной грамматике и ЬЦ1)-грамматике;

3. Разработать инструментальное средство для конструирования и применения в составе прикладных программ транслирующих ПОФ;

4. Применить разработанное инструментальное средство на практике.

Объектом исследования является теория и практика спецификации

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

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

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

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

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

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

Разработанные алгоритмы преобразования регулярных и ЬЦ1)-грамматик в ПОФ могут быть использованы для построения более сложных инструментов решения задач трансляции на основе формул первопорядковой логики.

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

Разработанное инструментальное средство компонент синтеза транслирующих программ (КСТП), алгоритмы преобразования грамматик в ПОФ и представление требований к диалогу в виде ПОФ применены при решении двух практических задач: разработки учебных трансляторов и контроля диалога в диалоговой системе Терминал.

Достоверность результатов. Достоверность полученных в работе результатов подтверждена разработкой алгоритмов построения ПОФ по регулярным и ЬЦ1)-грамматикам и доказательством эквивалентности грамматического разбора регулярных и 1Х(1)-языков процессу доказательства существования соответствующей транслирующей программы.

Эффективность полученных в работе результатов подтверждена опытом практической эксплуатации разработанного автором инструментального средства. Данное инструментальное средство применяется при решении учебных задач трансляции в ИМЭИ ИГУ в рамках курса «Языки программирования и методы трансляции» с 2007 г. по настоящее время. С помощью КСТП решена задача контроля диалога в рамках специализированной диалоговой системы таможенного контроля лесоматериалов. Диалоговая система контроля лесоматериалов рекомендована Федеральной таможенной службой России к экспериментальному опробованию в таможенных органах Сибирского таможенного управления и Дальневосточного таможенного управления1.

Соответствие диссертации паспорту научной специальности. В диссертации представлена новая модель и схема решения задачи трансляции в исчислении ПОФ. Результаты работы могут быть использованы при проектировании прикладных программ и систем, включающих трансляцию формальных языков. Одним из аспектов использования является контроль допустимости цепочек входных воздействий в составе диалогового интерфейса прикладной программы. Таким образом, тематика диссертации соответствует пунктам 1, 7 области исследований специальности 05.13.11.

Апробация работы. Основные результаты работы были представлены на научно-теоретической конференции молодых ученых, посвященной 60-летию Великой Победы (Иркутск, 2005), на VII Всероссийском симпозиуме по прикладной и промышленной математике (Кисловодск, 2006), на VIII школе-семинаре молодых ученых «Математическое моделирование и информационные технологии: управление, искусственный интеллект, прикладное программное обеспечение, технологии программирования» (Иркутск, 2006), на IX школе-семинаре молодых ученых «Математическое моделирование и информационные технологии» (Иркутск, 2007), на XIV Байкальской Всероссийской конференции «Информационные и математические технологии в науке и управлении» (Иркутск, 2009), на III школе-семинаре молодых ученых «Инфокоммуникационные и вычислительные технологии и системы» (Улан-Удэ, 2010), на 4-й Всероссийской мультиконференции по проблемам управления (с. Дивноморское, 2011) и неоднократно на семинарах Института динамики систем и теории управления СО РАН и Кафедры информационных систем Института математики, экономики и информатики ГОУ ВПО ИГУ.

Результаты диссертации были получены в рамках проекта СО РАН «Интеллектные методы и инструментальные средства создания и анализа интегрированных распределенных информационно-аналитических и вычислительных систем для междисциплинарных исследований с

1 О распространении системы электронного поштучного учета: Письмо ФТС России от 11 марта 2008 г. № 01-11/9055).

применением ГИС, СНЮ и WeЬ-технологий» (№ гос. регистрации 01.2.00708582), 2007-2009 гг.

Публикации и личный вклад автора. По теме диссертации опубликовано 12 работ, которые включают 3 статьи [1-3] в журналах, рекомендованных ВАК для опубликования результатов диссертаций, 3 публикации [6, 11, 12] в трудах региональных и всероссийских конференций, 5 публикаций [4, 5, 7, 8, 10] в научных сборниках и журналах, 1 свидетельство об официальной регистрации программ в Федеральной службе по интеллектуальной собственности, патентам и товарным знакам [9].

Результаты главы 1 опубликованы в работах [1, 4, 5, 7]; результаты главы 2 опубликованы в [1, 2, 4, 5, 7, 8]; результаты главы 3 опубликованы в [1, 3,6,10,12]; результаты главы 4 опубликованы в [2,3, 8,9,11].

Все результаты, выносимые на защиту, получены автором лично. В работах [1, 3-5, 7] В.И. Курганскому принадлежат постановки исследуемых задач. В работах [2, 8] О.В. Курганской принадлежат результаты по диаграммному представлению ПОФ. В работе [9] Ю.Д. Королькову и В.И. Курганскому принадлежит решение вопросов, связанных с технологией, организацией и осуществлением учебного процесса.

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

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

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

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

Исчисление 3 построено в языке ПОФ I. Язык X - полный язык первого порядка, формулы которого имеют древовидную структуру.

Алфавит языка Ь описывается множеством символов следующих видов:

• х, у, г, ... - символы, обозначающие переменные;

• а, Ь, с, ... -константы;

• >,=,Л,В,... - предикатные символы различной арности;

• (,) - запятая, скобки для уточнения строения формул;

• V, 3 - знаки для кванторов всеобщности и существования соответственно.

Атомы языка Ь имеют вид —> '*)> где Л* - предикатный символ арности А, а каждое (/ = 1, ..., к)- переменная или константа.

Конечное множество атомов, записанных через запятую, и пропозициональные константы Т (истина) и Г (ложь) являются конъюнктами в языке Ь.

Элементарные формулы языка Ь имеют вид:

• 3 -формулы: ЗХ:А;

• V-формулы: ЧХ: А ЭР,

где X - множество переменных, А - конъюнкт.

Если Ф = {Ф|, ..., Фк) является множеством V-формул, то ЗУ:ВФ

является 3 -формулой. При к > 2 ветвление формул множества Ф понимается как конъюнктивное.

Если <Р = {Ч/1, ..., Ч^} является множеством 3-формул, то УУ-.ВЧ' является V-формулой. При к £2 ветвление формул множества *Р понимается как дизъюнктивное.

Далее записью ЭХ: А Ф} будем обозначать формулы языка

ПОФ2. Другой способ записи формул языка I имеет вид

где *Р - множество 3 -формул, принадлежащих языку Ь, Ф - множество ветвей вида

Ч*,, ..., Ч^ - множество V-формул, принадлежащих языку!.

Исчисление У в языке Ь имеет единственное правило вывода со, основой которого является понятие подстановки в.

Любой непосредственный последователь \/У:В базы 3X \ А называется вопросом к базе 3Х:А. Говорят, что вопрос У¥:В к базе ЗХ:А имеет ответ (ответную подстановку) в тогда и только тогда, когда в есть суть отображение УX и ВОсА.

Пусть ПОФ Е имеет вид УТ{*Р, ЗХ: А Ф}, а Ф содержит подформулу У7:5{3г| , тогда результатом аР применения правила вывода со

к вопросу \fY\B с соответствующей ответной подстановкой 9 будет формула ^ = {3* и 2,: А и С,9 Ф и %9}ыГк}.

2 Vassilycv S.N., Davydov A.V., Zherlov A.K. Intelligent control via new efficient logics // Proc. of the 17th IF AC World Congress. Seoul (Korea), 2008. P. 13713-13718.

def

ac.-.z.fr

3Q :Zk{4>k

Логический вывод ПОФ в исчислении ./ представляет собой цепочку эквивалентных преобразований исходной формулы F по правилу а, заканчивающуюся формулой V: ТЗ: Р. Если ПОФ не содержит ветви 3:К, то она невыводима.

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

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

. (уХ: (Р(Х) —> ЗУ: R(X, У)))

0)

(((vxt -.(pM^by, -.RjX,, У^л... ~ ^...л{\/Х„ :(Pn(X„)^3Yn:Rn{X„,Y„))l

где VX,:^,)-*^:^,^)), ..., VX„ :{РЯ(ХИ)->ЭГ.: VJf:{P(X)~*3Y:R(X,Y)) - спецификации транслирующих подпрограмм Gj, ..., G„ и транслирующей программы G соответственно. Формулы ■■•> Р&Х играют роль предусловий рассматриваемых

программ, аформулы Л,^,,}^),..., Rn(Xn,Y„), У) - их постусловий.

Элементы фг,), ..., Рл(х„), р(х) и Ф„Х), R(X,y)

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

На языке ПОФ теорема (1) имеет вид:

F = V:T UB{UQ, (2)

где база ПОФ UB = ЭХ: Р(х), а множество вопросов Ue=Ql, .... QnVY-.R{X,Y)lV, Часть V:T в

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

Формулы вида (2) позволяют решать задачу трансляции. Далее такие формулы будем называть распознающими позитивно-образованными формулами.

Для решения задачи трансляции с помощью распознающих ПОФ примем ряд соглашений:

• при описании структуры цепочки используются нетерминальные и терминальные символы;

• разбор входной цепочки выполняется слева направо по одному символу;

• конец входной цепочки обозначен специальным терминальным символом;

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

С учетом представленных соглашений дополним правило вывода ПОФ со новой стратегией вывода т.

Обозначим через р, а1 и ю2 составные элементы стратегии вывода г.

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

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

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

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

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

Транслирующие ПОФ отличаются от распознающих формул двумя моментами:

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

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

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

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

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

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

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

Алгоритм построения распознающей позитивно-образованной формулы С) = УТ ив\и„ для регулярной грамматики включает начальную установку позитивно-образованной формулы Рк, циклическую обработку правил грамматики О и циклическую обработку элементов входной цепочки С.

Начальная установка. Если входная строка имеет вид С = с,, положим ив =Эк: и = \, Р(сь и), РТф), £>(Я), иначе, если С = с1,...,с„, п>1, положим ив =3и:и = 1, Р^и), Определим множество вопросов

одним вопросом 11д = {\/:ЛГ(#)3:Р. Здесь атом Р(си и) символизирует

возможность разбора входного элемента с,, расположенного в позиции и входной цепочки; атом РТ(#) означает возможность разбора символа конца входной цепочки #, а атом 2(5) символизирует разбор конструкции, обозначенной нетерминальным символом 5 (нетерминальным символом Я обозначена аксиома грамматики).

Обработка правил грамматики й.

1. Для каяедого правила вида 2 -> аУ (где 2 е К„, аеУт) пополним ив вопросом \/.у :Р(а,х), (2(2) 3: 2(к). Атом .?) означает успешный разбор входного элемента а, расположенного в позиции ^ входной цепочки.

2. Для каждого правила вида (где 2 еУм, а е Уг) пополним ид вопросом V.?: Р(а,.?), РТф), 0{2) 3: ЛТ(#). Атом ЯТ(#) указывает на успешный разбор символа конца входной цепочки.

Обработка элементов входной цепочки С-с„...,с„, п> 1:

1. Для каждого символа исходной цепочки с, (¿=1,...,«-2) пополним ид вопросом V.? :.? = /, Л(с,.,5)3:5 = »'+1, Р(сих,з);

2. Для символа исходной цепочки спА пополним множество вопросом V.?: 5 = и -1, 7?(с„_, = Р(сп^), РТ(#).

Утверждение 1. Для всякой праволинейной детерминированной регулярной (автоматной) грамматики (? и входной цепочки С формула С) доказуема тогда и только тогда, когда С е 1(<?), где ¿(с?) означает множество цепочек, порождаемых грамматикой б.

Алгоритм построения ПОФ (б, С) = УТII в \и0 для ЬЦ1)-

грамматики также включает в себя начальную установку, циклическую обработку правил грамматики (7 и циклическую обработку элементов входной цепочки С:

Начальная установка Определим базу ПОФ ив=3и: и-1, Р(сьи),

6(5), ЕОР(). Зададим множество вопросов £/с> - {V: РТ(#\ ЕОР{) 3: Р.

Здесь атом ЕОР() указывает на успешное завершение разбора входной цепочки.

Обработка правил грамматики б.

1. Для каждого правила вида 2-^ау (где аеУт, уеУ*) пополним 1/д вопросом Запись \у] означает преобразование цепочки у = у1 ...ук е (Ут иУ^) в конъюнкт по следующим правилам. Если выполнено условие У1^УТ, то (/,]= где атом КТ(у1) символизирует успешный разбор символа у,. Если выполнено условие У, еУ„,то Ы=б(Г/).

2. Обозначим через

множество направляющих символов правила 2 . Для каждого правила вида (где у = Ар,

Ае Уы, уЗеК*) и каждого г е ВБ^, у) пополним ие вопросом

3. Для каждого терминального символа / е Ут и правила Z -> а/Д (где 2еУх , аеУ+, /?е У*) пополним ид вопросом V*:я), 5).

4. Введем символ конца исходной цепочки #, #<£(УтиУы). Для каждого правила вида 2 в и элемента г б пополним вопросом :/'(/, 4 6(^)3л), если и вопросом V.?:РТ{#\ РТ(#), если / = #. Символ г обозначает пустую цепочку.

Обработка элементов входной цепочки С.

1. Для каждого символа входной цепочки с,, /<и, пополним вопросом

2. Для символа с„ пополним вопросом = Л(сп,з)Э:РТ(#).

Утверждение 2. Для всякой 1Х(1)-грамматики (7 и входной цепочки С

формула Г1Х(С,С) доказуема тогда и только тогда, когда С е

Ф).

Утверждения 1 и 2 доказаны математической индукцией по количеству шагов грамматического разбора входной цепочки и количеству шагов вывода соответствующей ПОФ.

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

3 См., например, Ахо А., Сети Р., Ульман Д. Компиляторы: принципы, технолог™ и инструменты: Пер. с англ. М.: Изд. дом «Вильяме», 2001. 768 с.

Компонент синтеза транслирующих программ обеспечивает:

• конструирование и испытания на примерах транслирующих ПОФ при проектировании прикладной программы;

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

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

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

Все эти экземпляры классов представлены коллекциями. Коллекции формируются, например, из атомов, составляющих конъюнкт, или из аргументов атома. Транслирующая ПОФ в целом представлена следующими коллекциями:

• переменных вывода при корневом кванторе существования транслирующей ПОФ;

• пар атомов и связанных с ними команд запуска транслирующих подпрограмм в составе конъюнкта при корневом кванторе существования транслирующей ПОФ;

• вопросов в составе формулы транслирующей ПОФ.

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

Формальная грамматика в КСТП представлена классом контекстно-свободных грамматик и его наследниками - классами регулярных и LL(1)-грамматик. Классы регулярных и 1А(1)-грамматик отличаются друг от друга функциональными членами, предназначенными для контроля и преобразования грамматики в ПОФ.

Управление экземпляром КСТП при исполнении прикладной программы обеспечивается обращением к его функциональным членам. Среди функциональных членов КСТП основными являются методы Prove, Synthesize и Execute, предназначенные для осуществления доказательства ПОФ, синтеза транслирующей программы и исполнения транслирующей программы соответственно.

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

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

Синтез и исполнение транслирующей программы также может осуществляться в двух режимах: по мере выполнения успешных шагов доказательства ПОФ или после завершения доказательства.

КСТП разработан в MS Visual Studio.Net 2005 и реализован на языке С#.

Ниже представлен сравнительный анализ КСТП с другими средствами разработки трансляторов.

КСТП Prolog YACC

Решение задач лексического анализа + + -

Решете задачи синтаксического анализа + + +

Работа с ^-грамматиками + +

Интеграция в прикладную программу В виде программного компонента Вызов внешнего интерпретатора Prolog В виде сгенерированного кода

Размер исходного кода транслятора для задачи распознавания арифметических „4 выражении -24 вопроса -35 предложений -40 строк

Отладка транслятора + - -

Автоматическое исправление ошибок при трансляции + + -

Графический интерфейс + - -

Четвертая глава посвящена применению КСТП для решения практических задач.

Первой задачей является задача конструирования учебных трансляторов. Конструирование трансляторов является частью учебных курсов по соответствующим дисциплинам. Учебный транслятор представляет собой GUI-приложение платформы .Net. Для решения этой задачи транслятор задается несколькими экземплярами КСТП (по одному для каждого типа лексем и один для синтаксиса входного языка) и программным кодом объемом около 100 строк исходного текста для управления процессом трансляции. Все шаги этого процесса (разбор входных цепочек, синтез и исполнение транслирующих программ) обеспечиваются обращением к функциональным членам соответствующих экземпляров КСТП.

Конструирование транслирующих позитивно-образованных формул обеспечивается соответствующими экземплярами КСТП при проектировании учебного транслятора в инструментальной среде Microsoft Visual Studio.Net.

Все остальные действия, связанные с разработкой учебного транслятора, обеспечиваются штатными средствами интегрированной среды разработки Microsoft Visual Studio.Net.

4 Cohen J., Hickey T.J. Parsing and compiling using Prolog // ACM Transactions on Programming Languages and Systems (TOPLAS). 1987. Vol. 9, Issue 2. P. 125-163.

Технология решения учебных задач трансляции в среде Microsoft Visual Studio.Net внедрена в Институте математики, экономики и информатики Иркутского государственного университета. Набор компонентов, обеспечивающих данную технологию, включает KCÏTÏ и зарегистрирован Иркутским государственным университетом в Федеральной службе по интеллектуальной собственности, патентам и товарным знакам.

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

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

В соответствии с решением коллегии Федеральной таможенной службы России средство таможенного контроля Терминал принято к экспериментальному опробованию в составе новой технологии контроля необработанных лесоматериалов5.

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

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

ОСНОВНЫЕ РЕЗУЛЬТАТЫ РАБОТЫ

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

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

5 О распространении системы электронного поштучного учета: Письмо Федеральной таможенной службы России от 11 марта 2008 г. № 01-11/9055.

на основе исчисления ПОФ. Разработаны алгоритмы построения ПОФ по грамматикам регулярных и ЬЦ1)-языков. Доказана эквивалентность грамматического разбора этих языков процессу вывода ПОФ.

2. Создано инструментальное средство для конструирования и применения транслирующих ПОФ в составе прикладных программ.

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

ОСНОВНЫЕ ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Бутаков М.И., Курганский В.И. О решении задачи трансляции планированием вычислений на основе позитивно-образованных формул // Системы управления и информационные технологии. 2007. №3.1(29). С. 120-123.

2. Бутаков М.И., Курганская О.В. Решение учебных задач трансляции на основе позитивно-образованных формул // Системы управления и информационные технологии. 2008. № 3.1 (33). С. 124-128.

3. Бутаков М.И., Курганский В.И. Контроль диалога объектных программ на основе позитивно-образованных формул // Вопросы современной науки и практики. Университет им. В.И.Вернадского. 2010. №4-6(29). С. 106-115.

4. Курганский В.И., Бутаков М.И. Лексический анализ на основе регулярных грамматик и конечных автоматов // Иркутск: Иркут. гос. ун-т. 2006.20 с.

5. Курганский В.И., Бутаков М.И. Синтаксический анализ на основе 1А(1)-грамматик и автоматов с магазинной памятью. Иркутск: Иркут. гос. ун-т, 2006. 32 с.

6. Бутаков М.И. Компонент построения и исполнения транслирующих программ на основе позитивно-образованных формул // Материалы IX школы-семинара молодых ученых «Математическое моделирование и информационные технологии» (Иркутск, 22-27 октября 2007 г.). Иркутск: РИО ИДСТУ СО РАН, 2007. С. 36-39.

7. Бутаков М.И., Курганский В.И. Об одной модели трансляции на основе позитивно-образованных формул // Информационные технологии моделирования и управления. 2007. № 6 (40). С. 663-672.

8. Бутаков М.И., Курганская О.В. Лексический анализ: обучение моделированию и программированию // Информационные технологии моделирования и управления. 2008. № 2 (45). С. 128-135.

9. Корольков Ю.Д., Курганский В.И., Бутаков М.И. Набор компонентов Рагееилк: Свидетельство об официальной регистрации программы для ЭВМ

№ 2007611658 от 20.04.2007 г. М.: Федеральная служба по интеллектуальной собственности, патентам и товарным знакам, 2007.

10. Бутаков М.И. Компонент построения и исполнения транслирующих программ на основе позитивно-образованных формул // Прикладные информационные технологии и системы. Иркутск: Изд-во Иркут. гос. ун-та, 2009. С. 4-27.

11. Бутаков М.И., Контроль входных воздействий в специализированной системе // Тр. XIV Байкальской Всерос. конф. «Информационные и математические технологии в науке и управлении». Ч. II. Иркутск: ИСЭМ СО РАН, 2009. С. 105-115.

12. Бутаков М.И. Инструментальное средство синтеза и исполнения транслирующих программ на основе позитивно-образованных формул // Материалы 4-й Всерос. мультиконф. по проблемам управления. Таганрог: Изд-во ТТИ ЮФУ, 2011. Т. 1. С. 27-29.

Редакционно-издательский отдел Учреждения Российской академии наук Института динамики систем и теории управления Сибирского отделения РАН 664033, Иркутск, ул. Лермонтова, д. 134 E-mail: rio@icc.ru

Подписано к печати 22.12.2011 г. Формат бумаги 60x84 1/16, объем 1,2 п.л. Заказ 36. Тираж 120 экз.

Отпечатано в ИДСТУ СО РАН

61 12-5/1916

РОССИЙСКАЯ АКАДЕМИЯ НАУК /

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

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

Бутаков Михаил Игоревич

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

формул

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

Диссертация на соискание ученой степени кандидата технических наук

Научный руководитель: к.ф.-м.н., доц. В.И. Курганский

Иркутск - 2011

Оглавление

Введение....................................................................... . 4

Глава 1. Синтез транслирующих программ на основе позитивно-образованных формул ..................................................................................14

1.1. Язык и исчисление позитивно-образованных формул...........................] 7

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

1.3. Конструктивный фрагмент исчисления позитивно-образованных формул для решения задач трансляции..........................................................25

1.4. Синтез транслирующих программ. Принципиальная схема решения задач трансляции на основе исчисления позитивно-образованных формул .............................................-.............................................................................29

1.5. Выводы .....................................................................................34

Глава 2. Регулярные и ЬЦ1)-грамматики. Существование транслирующей программы........................................................................................^

2.1. Распознающие позитивно-образованные формулы для регулярных правосторонних детерминированных грамматик..........................................37

2.2. Распознающие позитивно-образованные формулы для 1Х( 1 )-грамматик........................................................................................47

2.3. Выводы................................................................................................... 67

Глава 3. Компонент синтеза транслирующих программ.......................................68

3.1. Условия и общая схема применения компонента...................................69

3.2. Организация данных и диалоговый интерфейс компонента.................73

3.3. Выводы ................................................................................. . 75

Глава 4. Примеры применения компонента синтеза транслирующих программ ......................................................................................................................................84

4.1. Технология решения учебных задач трансляции....................................85

4.1.1. Учебные трансляторы. Требования и структура..........................90

4.1.2. Пример учебного транслятора.......................................................92

4.2. Контроль цепочек входных воздействий в диалоговой системе таможенного контроля Терминал....................................................................95

4.2.1. Назначение я структура диалоговой системы..............................96

4.2.2. Логико-лингвистическая модель диалога.....................................98

4.2.3. Реализация модели........................................................................Ю4

4.3. Выводы ..................................................................................¡05

Заключение..........................................................................................107

Литература..............................................................................] j j

Приложение 1. Множество направляющих символов для LL( 1 )-грамматик.... 123 Приложение 2. Акт об использовании результатов работы....................................................125

При решении прикладных задач часто приходится решать задачи трансляции. Примерами программ, где решаются задачи трансляции, являются: AutoCad [37], Microsoft Office (VBA) [45], 1С ¡Предприятие [44], предметно-ориентированные языки и системы программирования и др [64].

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

Одним из подходов к решению указанных задач является представление формального языка и входной цепочки в виде логической теории первого порядка [621. Применение логических средств для решения задач трансляции позволяет:

• Адаптировать средства интеллектуализации к терминологии и свойствам предметной области;

• Сократить время и трудоемкость разработки прикладных программ

со встроенными средствами трансляции;

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

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

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

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

4

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

Работа основана на результатах, полученных Васильевым С.Н. и его учениками в области логического вывода и приложений логического вывода в составе пакетов прикладных программ; Ершовым А.П. в области доказательного программирования; Манна 3. и Уолдингером Р. в области дедуктивного синтеза программ; Тыугу Э.Х. в области структурного синтеза программ. Существенное влияние на результаты диссертации оказали работы Н. Хомского, А.Ахо и Дж.Ульмана, посвященные моделям и методам трансляции.

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

Цель работы - обеспечить разработку и применение транслирующих программ в составе прикладных программ для формальных языков 2 и 3 классов по Хомскому [67] на основе позитивно-образованных формул.

Для достижения указанной цели были поставлены следующие задачи:

1. Разработать постановку и схему решения задачи трансляции в исчислении ГТОФ;

2. Разработать алгоритмы построения распознающих ПОФ по регулярной правосторонней детерминированной грамматике и Щ 1 )-

грамматике;

3. Разработать инструментальное средство для конструирования и применения в составе прикладных программ транслирующих ПОФ;

4. Применить разработанное инструментальное средство на практике.

Объектом исследования является теория и практика спецификации

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

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

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

Научную новизну диссертационного исследования составляют:

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

2. Инструментальное средство для конструирования транслирующих программ и их применения в составе прикладных программ, отличающееся от известных использованием универсального распознавателя КС-языков в виде ПОФ.

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

каждый из которых задается ПОФ. Схема отличается от известных

применением ПОФ.

4. . Постановка и схема отличаются от известных использованием ПОФ.

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

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

Представленные алгоритмы преобразования регулярных и ХХ(1)-грамматик в ПОФ могут быть использованы для построения более сложных инструментов решения задач трансляции на основе формул первопорядковой логики.

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

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

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

Эффективность полученных в работе результатов подтверждена опытом практической эксплуатации разработанного автором диссертационной работы и в струм ентал ьного средства. Данное инструментальное средство применяется при решении учебных задач трансляции в И МЭИ ИГУ в рамках курса «Языки программирования и методы трансляции» с 2007 г. по настоящее время. С помощью КСТП решена задача контроля диалога в рамках специализированной диалоговой системы контроля лесоматериалов. Диалоговая система контроля лесоматериалов рекомендована ФТС России к экспериментальному опробованию в таможенных органах СТУ и ДВТУ!.

Соответствие диссертации паспорту научной специальности. В диссертации представлена новая модель и схема решения задачи трансляции в исчислении ГЮФ. Результаты работы могут быть использованы при проектировании прикладных программ и систем, включающих трансляцию формальных языков. Одним из аспектов использования является контроль допустимости цепочек входных воздействий в составе диалогового интерфейса прикладной программы. Таким образом, тематика диссертации соответствует пунктам 1, 7 области исследований специальности 05.13.11.

Апробация работы. Основные результаты работы представлены на научно-теоретической конференции молодых ученых, посвященной 60-летию Великой Победы (Иркутск, 2005), на VII Всероссийском симпозиуме по прикладной и промышленной математике (Кисловодск, 2006), на VIII школе-семинаре молодых ученых «Математическое моделирование и

10 распространении системы электронного поштучного учета. Письмо ФТС России от 1 ] марта 2008 №0111/9055)

информационные технологии: управление, искусственный интеллект, прикладное программное обеспечение, технологии п рограм м ирования» (Иркутск, 2006), на IX школе-семинаре молодых ученых «Математи чес кое моделирование и информационные технологии» (Иркутск, 2007), на XIV Байкальской Всероссийской конференции «Информационные и математические технологии в науке и управлении» (Иркутск. 2009), на III школе-семинаре молодых ученых «Инфокоммуникационные и вычислительные технологии и системы» (Улан-Удэ, 2010). на 4-й Всероссийской мультиконференции по проблемам управления (с. Дивноморское, 2011), на объединенном семинаре Института динамики систем и теории управления СО РАН (2008), на кафедре информационных систем Института математики, экономики и информатики ГОУ В ПО ИГУ (2010).

Результаты диссертации были получены в рамках проекта СО РАН «Интеллектные методы и инструментальные средства создания и анализа интегрированных распределенных информационно-аналитических и вычислительных систем для междисциплинарных исследований с применением ШС, СШВ и \¥еЪ-технологий» (№ гос. Регистрации 01.2.00708582), 2007-2009

Публикации и личный вклад автора. По теме диссертации опубликовано 15 печатных работ, включая 3 статьи [10, 17, 18] в журналах, рекомендованных ВАК для опубликования результатов диссертационных работ, 5 публикаций [8, 11, 12, 13, 15] в трудах региональных, всероссийских, 6 публикаций [9, 16, 19, 38, 39, 40] в научных сборниках и журналах, 1 свидетельство [55] об официальной регистрации программ в Федеральной службе по интеллектуальной собственности, патентам и товарным знакам.

Результаты главы 1 опубликованы в работах [18, 19, 38, 391; результаты главы 2 опубликованы в [16, 17, 18, 19, 38, 39]; результаты главы 3 опубликованы в [8, 9, 13, 14, 18]; результаты главы 4 опубликованы в [10, 11, 12, 15, 17,39,55].

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

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

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

ПОФ.

2. Алгоритмы построения распознающих позитивно-образованных формул по заданным грамматикам: регулярной правосторонней детерминированной грамматике и ЬЦ1 )-грамматике. Для этих грамматик доказана эквивалентность доказательства теоремы существования транслирующей программы преобразованиями распознающей позитивно-образованной формулы и грамматического вывода.

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

4. Постановка и схема решения задачи контроля диалога человека и объектной программы на основе формальной спецификации требований к диалогу двухуровневой иерархией формальных языков, каждый из которых задается ПОФ. Задача контроля диалога решена применением КСТП.

Диссертация состоит из введения, четырех глав, заключения, библиографии и двух приложений. Общий объём диссертации - 123 страниц. Библиография включает 103 наименования. Работа иллюстрирована 20 рисунками и содержит 4 таблицы.

Глава 1 посвящена постановке и схеме решения задачи трансляции на

основе логического вывода в частном случае конструктивного фрагмента

10

исчисления позитивно-образованных формул. В пункте 1.1. приводится описания языка позитивно-образованных формул и построенного в данном языке исчисления. Язык ПОФ является языком первого порядка. Исчисление ПОФ состоит из одного правила вывода. Суть доказательства ПОФ - ее последовательное преобразование с помощью правила вывода. Пункт 1.2 посвящен доказательству существования транслирующих программ в исчислений ПОФ. Под транслирующей программой понимается программа, которая принимает на вход цепочку символов (исходный код), представленную на одном языке, и преобразует её в выходную цепочку символов (объектный код) на другом языке. Пункт 1.3 посвящен описанию подмножества языка ПОФ и выделению частного случая конструктивного фрагмента исчисления позитивно-образованных формул для решения задач трансляции. Основу частного случая конструктивного фрагмента составляют формулы из описанного подмножества языка ПОФ, стандартное правило вывода о) [21] и новая стратегия вывода г, необходимая для учета особенностей задач трансляции. В п. 1.4 введено понятие транслирующей позитивно-образованной формулы и представлена принципиальная схема решения задач трансляции на основе исчисления позитивно-образованных формул, Принципиальная схема решения задачи трансляции основана на идее автоматического синтеза программ [23, 26, 31, 60, 62, 69 с. 242, 92, 93, 102], когда транслирующая программа строится доказательством теоремы ее существования из �