Delist.ru

МОДЕЛИРОВАНИЕ КОНСТРУКТОРСКОЙ СЕМАНТИКИ (10.09.2007)

Автор: Барков Игорь Александрович

Рассмотрим модель M = (A, J( некоторого языка L = { P, F, c } описания СиОИ, где A - универсум модели. Интерпретирующее отображение J задает соответствие символам языка L, определенным на универсуме A отношениям P, функциям F и константам c. Мы допускаем частичные функции и предикаты в качестве интерпретаций. Для фиксации неопределенных вычислительных ситуаций и построения монотонного процесса семантических вычислений в работе введены множества неопределенных значений {(1, … , (n} для термов и {(1, … , (n} для формул. Каждая пара ((i, (i(, i=1, … . n соответствует i – му виду неопределенной вычислительной ситуации. Теперь A+= A( {(1, … , (n} универсум расширенной модели описания СиОИ, B+= B( {(1, … , (n}, где B = {и, л} и B+( A+. Будем теперь рассматривать все частичные функции как полностью определенные функции, отображающие (A+)m = A+ ( … ( A+ в A+. Все m- арные частичные предикаты будем считать полностью определенными на (A+)m.

Предложена многозначная логика следующего вида:

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

Утверждение. Если p(x0, … , xm) - монотонный предикат, определенный на A+ и m ( l, то (( xk) p(x0, … , xm) и (( xk) p(x0, … , xm), где k = 0, … , m, являются монотонными предикатами.

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

- интерпретация символа P в модели Mk, k=1, 2. Аналогичное утверждение доказано для функционального символа F.

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

построены с помощью суперпозиции монотонных функций и предикатов. Тогда M имеет единственное обогащение M1, являющееся моделью теории T1 и интерпретация символа F (P) является монотонной функцией (монотонным предикатом).

Для рекурсивных определений вида (4.5) введено специального вида преобразование ( : M*( M* над множеством моделей M*.

Теорема. Преобразование ( : M*( M*, соответствующее аксиоме (4.5), монотонно, если функционал ([R] монотонен.

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

цепью моделей, полученную преобразованием (.

- расширение теории T с помощью определяющей аксиомы вида (4.5) для символа R; M – модель теории T и функционал ( непрерывен. Тогда

является наименьшая неподвижная точка функционала (;

e) r монотонна.

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

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

Пусть дана теория T=TH(TS в языке прикладного исчисления предикатов L сигнатуры ( , где TH – множество структурных аксиом. Пусть TS=TD(TC, где TD - аксиомы – определения предикатных и функциональных символов вида (4.3), (4.4), (4.5). Множество TH(TD представляет собой систему аксиом, определяющих сигнатуру (словарь) профессионального расширения базового языка и, одновременно, предикатных СиОИ ТС.

( MH ( MD ( М.

Задача семантического анализа конструкции формулируется теперь так. Дана (возможно частичная) параметризованная структурная конструкторская модель MH, проверить, является ли MH решением (моделью) системы логических соотношений TS. Теоретические основы этой задачи введены (глава 4) в виде пошагового процесса обогащения моделей до получения искомой. Если все аксиомы-ограничения на построенном обогащении M истинны, то M является моделью теории T, т.е. решением поставленной задачи. Если некоторые предикатные свойства на обогащении M получают значения л, то задачу построения модели теории T, удовлетворяющей начальным условиям MH будем называть некорректно поставленной, а параметризованное СКР – некорректным. Если некоторые предикатные свойства на обогащении M получают значения (i (i=1, … , n), то полученная частичная модель, во-первых, может быть недостроенной и автоматизированная система подскажет, что еще нужно сделать; во-вторых, может быть не пригодной к использованию из-за конструкторских ошибок; в-третьих, может быть вполне приемлемой (неопределенные значения появились из-за отсутствия в конструкции необязательных элементов). Сама теория T всегда считается непротиворечивой, а обогащение M по начальным условиям MH определяется единственным образом.

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

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

Для решения задачи автоматизированного синтеза конструкции разработана формальная система S[G, z] порождения СКР, где G является непустым множеством правил вывода вида

Понятие С Cостав n1:j1, ( , nk:jk

Атрибуты nk+1:jk+1, ( , nl:jl

Внешние nl+1:jl+1, ( , nm:jm . (5.1)

Пусть z - начальный элемент вида (n0, j0, p0(, где n0 – конструкторское имя изделия, j0 – конструкторский тип изделия, p0 – позиция начального элемента в СКР.

Определение. Деревом порождения в системе порождения S[G, z] будем называть помеченное упорядоченное дерево D, если выполнены следующие условия:

а) корень дерева D помечен начальным элементом вида (n0, j0, p0(;

входит в раздел параметров; Di содержит узел, помеченный (((, если имеется спецификация вида (5.1) и раздел «состав» не содержит ни одного элемента;

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

- обозначение базового типа данных.

Пример СКР приведен на рис.2.

Автоматизированный синтез СКР представляет собой процесс чередования шагов порождения и анализа до получения законченного СКР, являющегося приемлемой моделью М теории Т. Если шаг порождения является безвариантным, то он выполняется автоматизированной системой. В выполнении вариантного шага порождения участвует человек.

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

. (5.2)

Полученная формула является системой логических соотношений, представленных в виде конъюнктивной игровой формулы, определяющей множество допустимых СКР. Нашей задачей является их построение. В работе определена теоретико – игровая семантика задачи автоматического порождения СКР двумя игроками ( и (. Получены и исследованы дерево поиска решений и дерево решений. Дерево решений определяет класс допустимых решений формулы (5.2).

Теорема. В каждой игре один из игроков имеет выигрышную стратегию.

В рамках решения задачи автоматического синтеза СКР было формализовано техническое задание на проектирование изделия. Суть технического задания – определить некоторые дополнительные условия для решения системы логических соотношений (5.2). Все условия выбора игроком ( очередного шага были разбиты на два класса: постоянные и временные. Постоянные средства выбора характеризуют накопленные в конструировании закономерности. Постоянные условия выбора целесообразно включать в описание системы конструкторских понятий. Временные средства выбора применяются только в конкретной конструкции, исходя из соображений, придать изделию некоторые определенные свойства. Выделение временных условий в самостоятельную спецификацию представляет собой в нашей постановке задачи техническое задание на проектирование. Находящиеся в техническом задании условия выбора уточняют или перекрывают аналогичные, записанные в системе конструкторских понятий постоянные условия выбора.

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

загрузка...