Логические средства поддержки информационных технологий

О. А. Ильичева
Ростовский государственный университет

Аннотация:

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

Effectively executable logical tools are offered to represent the tasks and properties of different subject fields. Logical language includes negations, equality, modules. The semantics of this language allows making exact diagnosis of logical mistakes. Mathematical aspects are considerate to ground the approach.

Интенсивное развитие систем и технологий информационной поддержки различного рода практических задач обострило проблему достоверности создаваемых продуктов -- их соответствия поставленной цели. Даже в такой формализованной области, как реляционные базы данных, по признанию специалистов, "современная технология БД обеспечивает слабые возможности для поддержки и оценки непротиворечивости данных" (СУБД, 4, 1997). Формальные средства, широко используемые для представления знаний, в экспертных системах, логическом программировании, не всегда адекватны для задач анализа и обеспечения корректности производимых систем. Модели термов, лежащие в основе семантики традиционных логических языков, не позволяют привычно работать с равенством, диагностировать даже такие "простые" логические ошибки, как противоречие, переопределение, неопределенность функций и т.п. Между тем, именно логический аппарат, на наш взгляд, является наиболее подходящим средством для таких задач, как анализ состоятельности проектных решений и оценка последствий предпринимаемых действий, поддержка непротиворечивости хранимой информации и корректности модификаций -- т.е. обеспечение "правильности" работы сложно устроенных систем, чья статическая или динамическая структура представляет собой запутанный "клубок" зависимостей и взаимодействий разнородных элементов. Для этих целей можно использовать достаточно простой логический язык, но более выразительный, чем версии Пролога, со специально подобранной эффективной семантикой.

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

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

Подход. Использование подхода предполагает выполнение двух этапов. На первом этапе составляется описание исследуемого объекта в предлагаемом логическом языке. В описание включаются: перечень элементов, их атрибутов, отношений между ними, правила, индуктивно определяющие эти отношения и атрибуты (зависимости между элементами) и правила, задающие ограничения на зависимости -- условия "правильности" функционирования, аварийные ситуации и т.п. В целом, правила должны полностью определять требуемые свойства объекта и/или его поведение. Если необходима поддержка корректности трансформаций исследуемой системы, то аналогичным образом могут быть описаны и трансформационные преобразования. На втором этапе подключаются интерпретаторы спецификаций, цель которых -- построение логической модели объекта и проверка выполнимости требуемых свойств. В процессе интерпретации диагностируются кроме того логические ошибки -- противоречивость и неполнота представления объекта или проекта системы.

Языковые средства. Описание -- спецификацию $ S=(\Sigma,T)$ исследуемого объекта составляют сигнатура $ \Sigma$ и теория $ T= T_1\cup T_2$ -- множество аксиом, определяющих объект ($ T_1$) и ограничивающих его состояние или поведение ($ T_2$). На практике более адекватен многосортный логический язык, но для простоты изложения далее используется односортная сигнатура. Формально, $ \Sigma=(R,F,C)$, где $ R$ -- множество имен предикатов (отношений), $ F$ -- функций (атрибутов) и $ C$ -- констант, причем С не пусто и все константы различны. Отношение равенства считается встроенным (аксиомы равенства автоматически добавляются к $ T_1$). Константы кодируют элементы объекта (например, конструкции программ или технические узлы, устройства, модули и т.п.).

Обозначения: $ \Sigma_t$ -- множество замкнутых термов сигнатуры $ \Sigma$, $ V_\Phi$ -- множество переменных формулы $ \Phi$; для произвольного множества $ A$: $ A^*$ -- совокупность конечных списков над $ A$, $ a$ -- элемент $ A$, $ \boldsymbol a$ -- вектор таких элементов; для всякой алгебраической системы $ M=(A,i)A$ обозначает носитель, $ i$ -- интерпретирующее отображение на $ A$. Аксиомы $ T_1$ рассматриваются как индуктивные определения объявленных в $ \Sigma$ функций и отношений формулами вида

$\displaystyle \forall\, \boldsymbol x(\varphi(\boldsymbol x)\to \psi(\boldsymbol x))$   или$\displaystyle \quad \forall\, \boldsymbol x\in \theta(\varphi(\boldsymbol x)\to \psi(\boldsymbol x)),$ (1)

где $ \boldsymbol x$ -- вектор переменных, $ \varphi(\boldsymbol x)$ -- конъюнкция атомарных формул вида $ r_i(\boldsymbol t)$,
$ t_i(\boldsymbol x)=t_j(\boldsymbol x)$ или их отрицаний ($ r_j\in R$, $ t_i,t_j,\boldsymbol t$ -- термы сигнатуры $ \Sigma$); $ \psi(\boldsymbol x)$ -- конъюнкция атомарных формул вида $ r_k(\boldsymbol x)$ (определение отношения $ r_k\in R$) или $ f_k(\boldsymbol x)=t_k(\boldsymbol x)$ (определение функции $ f_k\in F$). $ \theta$ -- конечный список. При каждом отношении с отрицанием $ \neg p(\boldsymbol x)$, содержащемся в $ \varphi(\boldsymbol x)$, должен присутствовать конъюнкт $ q(\boldsymbol x)$, позитивно входящий в эту же формулу, такой, что $ V_p \subseteq V_q$ (т.о. $ q(\boldsymbol x)$ играет роль ограниченного квантора для $ \neg p(\boldsymbol x)$). Подкласс аксиом $ T_1$ образуют формулы без переменных: $ r(\boldsymbol c)$, $ \neg r(\boldsymbol c)$, $ f(\boldsymbol c)=c_f$, составляющие множество фактов $ T_0$ -- конкретных утверждений об объекте. Ограничения $ T_2$ задаются произвольными формулами первого порядка с ограниченными кванторами. Для спецификаций определено понятие корректности, включающее в себя свойства полноты определения функций, непротиворечивости относительно аксиом равенства и непротиворечивости относительно использования отрицаний. Более точно, спецификация $ S=(\Sigma,T)$ называется корректной, если она:
$ F$-полна: $ \forall\, t\in \Sigma_t$ $ \exists\, c\in C$: $ t=c$ -- логическое следствие $ T$ и $ T$ -- ациклична;
$ E$-непротиворечива: $ \forall\, c_i,c_j$, $ i\ne j$, $ c_i=c_j$ не является следствием $ T$;
$ N$-непротиворечива: $ \Phi{\&}\neg\Phi$ не является следствием $ T$ для всякой атомарной формулы $ \Phi$. Требование ацикличности совокупности индуктивных определений гарантирует для каждой $ f(\boldsymbol c)$ существование хотя бы одного индуктивного доказательства $ f(\boldsymbol c)=c_f$, свободного от вхождений терма $ f(\boldsymbol c)$, т.е. исключает теории, редуцируемые к определениям вида $ t(f(\boldsymbol c))=t(f(\boldsymbol c))\to f(\boldsymbol c)=c_f$. Ацикличность дает возможность интерпретатору, реализующему вывод, не прибегая к дорогостоящему механизму унификации термов, получить значение определяемых функций за конечное число шагов, индуктивно вычисляя определяющие эти функции термы. Формально это свойство моделируется выводимостью в теории $ T_1^d$, полученной по $ T_1$ добавлением формул со специальным предикатом Def, контролирующим определенность термов [3]. Понятие $ N$-непротиворечивости для теории $ T_1$ отличается от обычной логической непротиворечивости, поскольку отрицания используются лишь в посылках $ \varphi(\boldsymbol x)$ импликаций, и сводится к непротиворечивости теорий $ T_1\cup\{\neg p(\boldsymbol c)\}$, в которой отношения $ p(\boldsymbol x)$ входят с отрицанием в формулы $ \varphi(\boldsymbol x)$. Фактически это означает, что ни одна замкнутая атомарная формула $ p(\boldsymbol c)$ не может быть выведена как следствие предположения об истинности $ \neg p(\boldsymbol c)$.

Семантика. Для обеспечения эффективной диагностики логических ошибок предлагается использовать в качестве семантики рассматриваемого класса спецификаций инициальные индуктивно-вычислимые (ИВ-) модели из констант $ C$. Модель такого типа строится по спецификации с помощью прямого вывода, в котором используются только подстановки констант вместо переменных. Поскольку тотальность функций требует существования следствий вида $ f(\boldsymbol c)=c_f$ для каждой $ f$, вывод по определениям $ T_1$ должен давать однозначное вычисление всех $ f\in F$. Единственность построения модели обеспечивает свойство инициальности, однако способ получения инициальных моделей $ M=(C,i)$ сам по себе не гарантирует вычислимости интерпретирующей функции $ i$. Поэтому выделен вычислимый подкласс таких моделей, семантически эквивалентных множеству синтаксически "хорошо определенных", т.е. корректных, спецификаций. Свойство индуктивной вычислимости фактически обеспечивает существование фундированного порядка на модели, при котором термы условия определения могут быть вычислены прежде определяемых значений и, таким образом, интерпретирующее отображение $ i$ может быть индуктивно вычислено по системе определений. Доказано [3], что такая модель однозначно соответствует корректной спецификации: Спецификация $ S=(\Sigma,T_1)$ имеет инициальную индуктивно-вычислимую модель
$ M=(C,i)$ из констант $ C$ тогда и только тогда, когда $ S$ корректна. Модель $ M$ может быть построена в соответствии с общим алгоритмом получения инициальных систем для квазитождеств [4]. В данном случае, поскольку носитель модели -- множество $ C$ и все константы различны, процесс порождения логических следствий теории $ T_1$ вида $ f(\boldsymbol c)=c_f$ и $ r(\boldsymbol c)$ фактически означает интерпретацию функций $ f\in F$ и отношений $ r\in R$ на $ C$. Для аксиом без отрицаний множество следствий образуется в результате обычного логического вывода. Атомарные замкнутые следствия всей теории можно получить, если задать интерпретацию для отношений $ \neg p(\boldsymbol x)$, входящих в $ T_1$ с отрицанием. Это означает попытку построения максимально непротиворечивого ($ N$-) расширения теории $ T_1$ формулами вида $ \neg p(\boldsymbol t)$, $ \boldsymbol t\in \Sigma_t^*$. Чтобы выявить возможность существования инициальной модели у таких спецификаций, необходимо принимать во внимание только строгие $ N$-расширения, в которых для всякого замкнутого следствия $ \psi(\boldsymbol t(\boldsymbol c))$ должно существовать определение, его "породившее", с истинной посылкой $ \varphi(\boldsymbol t(\boldsymbol c))$. Для произвольной спецификации вида (1) таких расширений может быть несколько. Доказано, что обладание инициальной строгой моделью для теории $ T_1$ равносильно существованию единственного строгого $ N$-расширения: Спецификация $ S=(\Sigma,T)$ имеет индуктивно-вычислимую инициальную строгую модель из констант тогда и только тогда, когда $ T_1$ имеет единственное $ E$-непротиворечивое и $ F$-полное строгое $ N$-расширение. Конструктивная проверка существования такого расширения и соответственно, процесс получения ИВ-модели сводится к построению множества стратегий интерпретации, каждая из которых однозначно соответствует некоторому отображению $ i$ и строгому $ N$-расширению, и проверке эквивалентности этих стратегий. Стратегия -- это фиксированная последовательность $ s$: $ \langle\langle p_1,c_1\rangle,\dots, \langle p_n,c_n\rangle\rangle$ выбора аксиом и конъюнктов, содержащих негативное вхождение предикатов $ p_j$. Элемент $ \langle p_j, c_j\rangle$ входит в стратегию $ s$, если на некотором шаге вывода неопределенный до этого на подстановке $ \boldsymbol x_j/\boldsymbol c_j$ предикат $ p_j(\boldsymbol x_j)$, был интерпретирован как ложный. Стратегия является непротиворечивой, если пересечение областей истинности и ложности всякого содержащегося в ней предиката $ p_j$ пусто (непротиворечивость базы данных). Это означает, что множество атомарных следствий теории $ T_1$, полученное интерпретацией $ i$ при стратегии $ s$, образует $ E$- и $ N$-непротиворечивую элементарную теорию. Стратегия $ s$ называется полной, если соответствующее множество следствий образует $ F$-полную теорию. Стратегии $ s_1$, $ s_2$ являются эквивалентными, если множества их элементов совпадают. Доказано, что Спецификация $ S$ обладает инициальной ИВ-моделью $ M$ тогда и только тогда, когда все непротиворечивые полные стратегии эквивалентны. Этот факт обосновывает анализ непротиворечивости спецификаций с отрицаниями. Ценность этого критерия в том, что гарантируется корректное построение минимальной модели, не требующее ограничений рекурсии в определениях и введения какого-либо упорядочивания или иерархии на множестве аксиом в $ T$, как, например, процедуры стратификации для обеспечения корректности обновлений в реляционных [6] или дедуктивных базах данных. Однако реализация этого критерия для конечных $ C$ в общем случае имеет экспоненциальную сложность. Условия понижения сложности интерпретации до полиномов низких степеней сводятся к критериям разрешимости проблемы существования модели с помощью единственной стратегии и к выделению ограничений, сокращающих перебор подстановок при определении истинности посылок (поскольку сам вывод линеен). Определен собственный подкласс индуктивно-вычислимых моделей, минимальная относительно гомоморфного вложения система в котором является инициальной в исходном классе. Такая модель может быть построена с помощью единственной стратегии и однозначно характеризует спецификацию с "хорошо определенной" рекурсией. Это свойство разрешимо со сложностью не более, чем $ O(n^2)$ относительно символьной длины теории и проверяется статически, без проведения интерпретации. Оно является более слабым ограничением, чем принятые в логических языках, допускающих отрицания, и запрещает только некоторые типы рекурсивной зависимости между отношениями, входящими с отрицанием в предложения $ T_1$.

Интерпретатор. Для обеспечения точности диагностики логических ошибок в качестве областей данных, на которых строится функция $ i$, рассматриваются полные решетки с низом -- "неопределенность" ($ \bot$), верхом -- "ошибка переопределения" ($ \top$) и отношением аппроксимации $ \subseteq$: для любого элемента $ x$ области $ X$ имеет место: $ \bot\subseteq x$, $ x\subseteq x$, $ x\subseteq \top$. Область значений истинности представляет $ \operatorname{Bool}=\{\bot, \operatorname{true}, \operatorname{false}, \top\}$. Логические операции -- конъюнкция, дизъюнкция, отрицание, а также равенство монотонно доопределяются на области $ \operatorname{Bool}$. Используются также монотонные "if... then... else" [5] и функция $ \max$, определенная на списках и равная максимальному по $ \subseteq$ элементу списка, причем $ \max(s)=\top$, если $ s$ содержит $ \top$ либо неравные элементы, т.е. $ \max(\top,x)=\top$; $ \max(x,y)=\top$, если $ x\ne y$. Интерпретатор вычисляет функцию $ i$ модели в соответствии с денотационными уравнениями [3], задающими отображение сигнатурных символов на множество функций и отношений на $ C$. Интерпретация $ i$ функций и формул на областях $ C=\{\bot,C,\top\}$ и $ \operatorname{Bool}$ определяется индуктивно по структуре термов и формул. Для символов сигнатуры $ f\in F$, $ r\in R$ выбирается максимальный по $ \subseteq$ элемент по всем определениям $ f$ и $ r$ в $ T_1$ и всем подстановкам $ \gamma$: $ X^*\to C^*$ в этих определениях. Монотонность дает возможность в случае возникновения ошибки переопределения доопределить на значение $ \top$ те функции и отношения, вычисление которых было "задето" ошибкой. Так фиксируется полный след ошибки и достигается однозначность результата интерпретации. Входом интерпретатора является исходное множество фактов, выходом -- диаграмма модели $ M=(C,i)$ -- множество замкнутых атомарных следствий теории $ T$. На полученной модели, если она существует, проверяются аксиомы $ T_2$. Алгоритм интерпретации состоит в поочередном выполнении двух шагов до тех пор, пока не будет получена неподвижная точка вычислений. На первом шаге интерпретируются определения, не содержащие отрицаний. Каждый полученный новый факт -- следствие инициирует выполнение правила, содержащего в посылке вхождение соответствующего отношения или функции. Ищется подходящая подстановка констант и определяется истинность левой части правила. Если значение интерпретации этой формулы -- истина или $ \top$, то определяемые в правой части отношения и функции на этой подстановке интерпретируются как истинные или равные $ \top$ соответственно. Полученные таким образом факты, если они являются новыми, продолжают активизировать действия шага 1. Если новых фактов нет (локальная неподвижная точка), начинается выполнение шага 2 -- интерпретация негативно входящих отношений, в соответствии с семантикой спецификаций с отрицанием. Новые факты $ \neg p(\boldsymbol c)$ (если они есть) инициируют выполнение определений с отрицаниями и повторение шага 1, если получены новые следствия. Доказано, что интерпретатор строит модель, если она существует, не зацикливается и завершает работу за конечное число шагов. Емкостная сложность интерпретации имеет порядок $ O(n)$, где $ n$ - мощность модели, временная оценивается произведением $ z*h*k$, где $ z$ -- сложность нахождения подходящих подстановок для одной аксиомы, $ h$ -- количество обращений к интерпретации аксиомы, $ k$ -- количество аксиом. Поскольку интерпретация предложений активизируется только получением нового факта, величина $ h$ не превышает $ n$. Значение $ z$ определяется как сложностью алгоритмов поиска подстановок в базе данных, так и видом зависимости переменных в условиях $ \varphi(\boldsymbol x)$ (типом графа, в котором отношения $ r_i$ -- дуги, а переменные $ x$ -- узлы). Если, например, граф зависимости представляет собой пучок или множество параллельных дуг, то $ z$ имеет порядок $ O(\log n)$.

Модули. Концепция и средства модульной логической спецификации основаны на идеях и методе параметризации и элементарной определимости моделей, изложенных в [2]. Пусть $ \Sigma_0=(R_0,F_0,C_0)$ -- некоторая базовая сигнатура, $ S_0=(\Sigma_0,T_0)$ -- спецификация, $ M_0=(C_0,i_0)$ -- ИВ-модель спецификации $ S_0$. Применяя используемый класс спецификаций в качестве порождающего механизма для получения ИВ-моделей, можно задать иерархию моделей, используя на первом шаге $ i_0$ как начальный вход для интерпретации рекурсивных определений некоторой спецификации $ S_1$, затем полученную модель $ M_1$ как базовую для следующей итерации $ (S_2,M_2)$ и т.д. Поскольку модели определяются вычислимыми спецификациями, процедура построения "модели моделей" конструктивна и позволяет обосновать процесс последовательного уточнения модулей. Пусть $ \Sigma_1=\Sigma_0\cup (R_p,F_p,C_p)$ -- обогащение $ \Sigma_0$, полученное добавлением предикатных ($ R_p$), функциональных ($ F_p$), константных ($ C_p$) переменных. Параметрическая спецификация (схема) $ S_p=(\Sigma_p,T_p)$ включает в качестве определяемых в $ T_p$ отношений и функций переменные (параметры) из $ R_p$ и $ F_p$; другие $ r\in R_p$, $ f\in F_p$, входящие в $ T_p$, рассматриваются как параметры со встроенной интерпретацией (внешние). Пусть $ i_0$ -- базовая интерпретация $ \Sigma_0$, $ \eta_0$ -- некоторая интерпретация внешних параметров, $ M_0=(C_0,i_0\cup\eta_0)$, $ \pi$ -- оператор, сопоставляющий при каждом означивании параметров $ \eta_0$ набору отношений и функций $ \psi_0$ из $ M_0$ набор $ \pi(\eta_0,\psi_0)$, определяемый как: $ \pi(\eta_0,\psi_0)=\{\boldsymbol c,\ M_0\vDash \varphi(\boldsymbol c,\eta_0)\to \psi_0(\boldsymbol c,\eta_0)\}$, где $ \{\forall\, \boldsymbol x(\varphi(\boldsymbol x)\to \psi(\boldsymbol x))\}$ входят в $ T_p$. Индуктивное определение: $ \pi_0(\eta_0,\psi_0)=\psi_0$; $ \pi_{n+1}(\eta_0,\psi_0)=\pi(\pi_n(\eta_0,\psi_0))$. Имеет место: Для каждых $ i_0$, $ \eta_0$ и параметрической спецификации $ S$ оператор $ \pi$ имеет неподвижную точку $ \pi_{\text{\rm fix}}$, являющуюся объединением $ \pi_n(\eta_0,\varnothing)$, $ n=1,\dots$ Теорема является следствием аналогичного результата для $ \Sigma^+$-программ [2]. Доопределим $ \eta_0$ до $ \eta$, поставив в соответствие определяемым параметрам из $ R_p$, $ F_p$ набор $ \pi_{\text{fix}}$. Пара $ (C,i_0\cup \eta)$ является моделью параметрической спецификации $ S$. Семантику $ S$ задает класс инициальных ИВ-моделей. В приведенной схеме в качестве input- и output-параметров могут выступать функции и отношения. Передача в качестве фактического параметра встроенной или уже полученной интерпретации -- аналог вызова-по-значению в процедурных языках -- означает передачу уже готового элемента модели, который не может быть доопределен. Передача параметра-модуля -- аналог вызова-по-имени -- означает передачу спецификации, которая может участвовать в порождении новой модели -- экземпляра схемы. Поскольку схема -- параметрическая спецификация представляет класс моделей, то точную диагностику ошибок можно провести только при интерпретации спецификации с конкретизированными параметрами. Однако, предварительная (статическая) диагностика может быть проведена интерпретацией схемы, где в качестве сигнатуры используются имена формальных параметров, а в качестве входа -- множество (параметризованных) фактов или пустое множество. При представлении трансформаций схема может быть частично параметризована и соответствующая модель -- "частично построена" (аналог смешанных вычислений). Диагностика такой спецификации также будет неполной, где неопределенность функции (не получение ею значения-константы) либо не считается ошибкой, либо снимается доопределением функции на значение невычисленного терма (т.е. константу представляет терм, символ которого включается во множество $ C$). В качестве модуля может выступать параметрическое определение отношения или функции, а также параметрическая спецификация (схема), используемая, например, как генератор типов. Соответственно параметром может быть модель (множество исходных фактов), множество констант, спецификация (определение конкретного отношения или функции), параметрическая спецификация (модуль). Анализ соответствия фактических и формальных параметров, идентификация переменных выполняются в рамках этого же подхода: аксиоматизируются правила "видимости" переменных и соответствия типов, контекстные условия и запускается интерпретатор, который в данном случае играет роль семантического анализатора, как это было сделано для языков программирования [1].

Трансформации и модификации. Преобразования моделируемого объекта сводятся к изменениям его логической модели (и, соответственно, спецификаций) которые можно представить комбинацией следующих базовых трансформаций: 1. Доопределение функций и отношений на исходном множестве $ C$ (задачи анализа). Пусть $ t_1,\dots,t_n$ -- последовательность трансформаций, реализующая преобразование объекта (программы, проекта, системы) из состояния $ \Omega_1$ в состояние $ \Omega_n$. В качестве логического представления трансформации $ t_i$ рассматривается спецификация $ S_i=(\Sigma_i,T_i)$, а сам процесс трансформации состоит в интерпретации $ S_i$ -- получении минимальной модели $ M_i=(C_i,I_i)$, представляющей семантику $ S_i$. Условием корректности всякой трансформации $ t_i$ тогда является условие правильности спецификации $ S_i$: У1). Трансформация $ t_i$ корректна тогда и только тогда, когда $ T_i$ имеет модель $ M_i$. Это условие эквивалентно непротиворечивости (относительно равенства и использования отрицаний) и $ F$-полноте спецификации $ S_i$. Условие У1 не ограничивает поведение последовательности трансформаций. Корректность всего цикла преобразований может потребовать выполнения дополнительных ограничений. Например, если для всякого $ i$ $ \Sigma_i=\Sigma_{i+1}$, то каждая $ I_{i+1}$ получена доопределением $ I_i$. Тогда имеем: У2) Последовательность $ t_1,\dots,t_n$ трансформаций корректна, если корректна каждая $ t_i$, и $ M_1\preccurlyeq M_2\preccurlyeq \dots \preccurlyeq M_n$, где $ \preccurlyeq$ -- отношение гомоморфного вложения. Условие У2 является достаточно слабым для последовательности трансформаций. В частности, оно не требует корректности совокупной спецификации $ S=(\Sigma,T_1\cup T_2\cup\dots\cup T_n)$. Поскольку допускаются формулы с отрицанием, и вывод с фактами, полученными на шаге $ i$ не повторяется для спецификаций $ S_j$, $ j<i$, то минимальная модель $ M$ для $ S$, хотя и может существовать, но не обязательно является объединением моделей $ M_i$. 2. Добавление новых элементов, отношений и атрибутов (пошаговое уточнение, задачи проектирования и синтеза). Если при преобразованиях $ t_i\to t_{i+1}$ сигнатура расширяется, т.е. $ \Sigma_i\subset \Sigma_{i+1}$, то корректность последовательности трансформаций поддерживает следующее условие: У3) последовательность трансформаций $ t_i\to t_{i+1}$ корректна, если корректна каждая из них и модель $ M_i$ является подсистемой $ M_{i+1}$ в сигнатуре $ \Sigma_i\cup \Sigma_{i+1}$, причем $ I_{i+1}\upharpoonright((R_i\cup F_i\cup C_i)\times C_i^*)=I_i$. Символ $ \upharpoonright$ обозначает операцию ограничения функции. 3. Сужение исходной логической структуры (удаление элементов, задачи оптимизации). Это немонотонное в общем случае преобразование, тем не менее, в ряде задач может быть представлено в рамках рассматриваемого класса спецификаций. В аксиомы $ T_i$ добавляется переменная времени или состояния, пробегающая конечный интервал, например, $ H=[h_1,\dots,h_n]$, $ h_j\in C$, "шагов": $ \forall\, y\in H$, $ \forall\, \boldsymbol x(\varphi(\boldsymbol x,y)\to \psi(\boldsymbol x,$next$ (y)))$. Корректность трансформаций $ t_i$ тогда определяется условием У1, а для их последовательности должно выполняться: $ I_{i+1}=I_i\upharpoonright((R_i\cup F_i\cup C_i)\times C_i^* \times h_{i+1})$. При добавлении в вектор аргументов переменной $ h_k$ метятся все элементы отношений, которые нужно "оставить". Это не всегда удобно, если работает рекурсивное правило, например, транзитивного замыкания отношения подчинения узлов на дереве. Заранее невозможно определить требуемое количество шагов, и непросто поэтому задать трансформацию, касающуюся последнего шага. В этих случаях удобнее использовать отношение "удален", помечающее элементы, которые можно "выбросить". Например, два следующих правила задают необходимое преобразование $ \psi(x,y)$ на последнем, уже сохраняемом элементе отношения:
    $\displaystyle \forall x,y,z \bigl(r(x,y) \&  r(y,z)\to (r(x,z)) \& $   удален$\displaystyle ($имя$\displaystyle (r),x,y) \& $   удален$\displaystyle ($имя$\displaystyle (r),y,z)\bigr);$  
    $\displaystyle \forall x,y \bigl(r(x,y) \&  \neg$   удален$\displaystyle ($имя$\displaystyle (r),x,y)\to \psi(x,y)\bigr).$  

В некоторых работах для спецификации удаляемого элемента отношения вводится отрицание в правую часть формулы: $ \forall\, \boldsymbol x(\varphi(\boldsymbol x)\to \neg r(\boldsymbol x))$. Такой подход, однако, требует определения нестандартной (нелогической) семантики отрицания, т.к. использование обычной семантики немедленно приводит к противоречию -- порождению и отрицанию элемента одновременно. Если трансформации выполняются асинхронно или параллельно, или проводится многоэтапная рекурсивная трансформация, то необходимым условием корректности трансформаций является существование для совокупной спецификации $ S$ минимальной модели, изоморфной объединению моделей $ M_i$. Условия корректности трансформаций связаны, как правило, не только с проблемой "хорошей определенности" спецификаций трансформаций, но и с предметной областью, с целями проводимых преобразований. Сохранение некоторых требуемых свойств (инварианты трансформации) может быть специфицировано явно, в виде аксиом-ограничений, проверяемых на уже полученной модели -- результате трансформации, или являться следствием условий корректности, налагаемых на последовательность преобразований в целом. Так, например, если преобразовывалась некоторая программа, то условие У2) гарантирует сохранение ее семантической функции.

Динамические взаимодействия. Возможность представления динамических свойств реализуется включением переменных времени в логические формулы. Эти переменные пробегают конечные отрезки $ T$ дискретного набора точек, каждая из которых может задаваться либо конкретной датой, либо событием (именем или сигналом события). Например, интерпретация предложения: $ \forall t$, $ t_0\in T$ ( сигнал$ (t_0) \&  t\geqslant t_0 \to$   режим$ (t)$) установит состояние режим для временных точек интервала $ T$ после момента $ t_0$ -- времени наступления события сигнал. Такого рода спецификации использовались для моделирования космических тренажеров, где время получения сигнала и входа в требуемое состояние было точно задано. Использование переменных времени позволяет обеспечить монотонность вычислений при интерпретации трансформаций структуры объекта или преобразовании модели, а также сохранять историю проекта в рамках единой языковой и инструментальной среды. Некоторые примеры спецификаций, использованных на практике, можно найти в [3] (прототипирование процесса космической стыковки) и в [1] (семантический анализ по спецификации статической семантики языков Алгол и Модула-2). Несмотря на сложное математическое обоснование, практические спецификации выглядят ясно и просто. Например, все правила видимости переменных в языке Модула-2 составляют четыре аксиомы-определения и две аксиомы-ограничения, описывающие контекстные условия.

Литература

  1. Глушкова В. Н., Ильичева О. А. К пpоблеме видимости и типизации в языке МОДУЛА-2. Язык МОДУЛА-2, его pеализация и использование. Сб. ВЦ СО РАH, Hовосибиpск, 1989.

  2. Гончаров С. С., Свириденко Д. И. $ \Sigma^+$-программы и их семантики. Вычислительные системы, 120, 1987, 24-51.

  3. Ильичева О. А. Средства эффективной диагностики ошибок для систем логического прототипирования. Автоматика и телемеханика, 9, 1997, 185-196.

  4. Мальцев А. И. Алгебраические системы. Наука, Москва, 1970.

  5. Манна З. Теория неподвижной точки программ. Кибернетический сборник, 15. Мир, Москва, 1978, 38-100.

  6. Louiqa Raschid, Jorge Lobo. Semantics for Update Rule Programs and Implementation in a Relational Database Management System. ACM Transaction on Database Systems, Vol.22, 4, 1996, 526-571.
Ваши комментарии
[SBRAS]
[Головная страница]
[Конференции]
[СО РАН]

© 2001, Сибирское отделение Российской академии наук, Новосибирск
© 2001, Объединенный институт информатики СО РАН, Новосибирск
© 2001, Институт вычислительных технологий СО РАН, Новосибирск
© 2001, Институт систем информатики СО РАН, Новосибирск
© 2001, Институт математики СО РАН, Новосибирск
© 2001, Институт цитологии и генетики СО РАН, Новосибирск
© 2001, Институт вычислительной математики и математической геофизики СО РАН, Новосибирск
© 2001, Новосибирский государственный университет
Дата последней модификации Thursday, 06-Sep-2001 14:19:12 NOVST