Программные продукты и системы

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

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

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

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

Синтаксис языка L

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

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

Множество команд  с типичным элементом  определим следующим образом:

,

где  – типичный элемент множества защищенных команд  со следующим синтаксисом:

,

,

.

Фигурные скобки используются в БНФ для обозначения нулевого либо большего количества повторений конструкции, заключенной в скобки. Через  обозначается типичный элемент множества защит , а через  – типичный элемент множества процессов . В дальнейшем круглые скобки в записи  опускаются там, где это не вызывает недоразумений.

Алгебраическая семантика: математические основы и семантические равенства

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

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

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

1);

2) .

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

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

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

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

Типичные элементы семантических областей могут иметь индексы.

Определим множество вычислительных последовательностей  с типичным элементом . Предварительно определим два дополнительных множества: множество тестов  с типичным элементом  и множество действий  с типичным элементом .

;

;

.

Заметим, что одни и те же элементы  могут использоваться в качестве и тестов, являющихся значениями защит команд, и действий, являющихся значениями команд. Элемент  – это значение, соответствующее взаимодействию команд  и , которые могут использоваться как в качестве защит, так и в качестве команд ввода/вывода.

Обозначим через  конечную ВП, а через  – бесконечную.

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

Определение 1. ВП  называется пустой и обозначается через , если ; .

Бесконечную последовательность вида  обозначим через  (зацикливание).

Определение 2. , если ;  и  принадлежит хотя бы одному из множеств  или ;  и  принадлежит и , и  одновременно.

Определим теперь  как минимальную фиксированную точку оператора , то есть , где  имеет вид:

,

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

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

Семантическая функция рассчитывается следующим образом:

1) ,

2) ,

3) ,

4) ,

5) ,

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

6) ,

7) ,

8) ,

9) ,

10) ,

11) ,

12) ,

13) ,

14) .

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

Определим теперь семантическую функцию для выражений :

1) ,

2) ,

3)

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

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

Определение 3. Процесс  называется помеченным меткой . При этом метка  называется родительской для процесса .

Определение 4 (правило дедукции). Пусть метка  является родительской для процесса . Тогда

1) если  либо , то метка  является родительской для  и ;

2) если  либо, то метка  является родительской для ;

3) если, в свою очередь, gc либо , то метка  является родительской для  и .

Определение 5. Пусть метка  является родительской для процесса . Тогда она будет прародительской (или родительской 2-го порядка) для процесса . При этом является родительской меткой 2-го порядка для всех компонентов процесса , рассмотренных в определении 4. Будем также говорить, что метка  будет в этом случае родительской для метки .

В общем случае понятие «родительский» можно обобщить, полагая, что, если метка  является родительской 1-го порядка (или просто родительской) для процесса , а метка  родительской k-го порядка для некоторого компонента процесса , то метка  является родительской (k+1)-го порядка для соответствующего компонента.

Определение 6. Родословной n-го порядка  для некоторого вхождения компонента  называется объединение родительских меток этого компонента с 1-го по n-й включительно.

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

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

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

Очевидно, что, если множество  состоит из одного компонента, то .

Лемма 1. Пусть  и  – компоненты программы . Тогда .

Доказательство. Тривиально, из определений 7 и 8.

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

Лемма 2.

а)

б)

в)

г)

д)

Доказательство. Тривиально, из определений 4, 8.

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

Лемма 3. Пусть  – подмножество компонентов программы  Тогда .

Доказательство. Тривиально, методом численной индукции.

Пример 1. Пусть дана программа

и пусть .

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

,

,

,

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

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

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

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

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

Аксиоматизация свойств семантической области. Для обозначения элементов семантической области используем метапеременные .

Аксиомы, задающие базисные свойства операций  и :

(A1) ,

(A2) ,

(A3) ,

(A4) ,

(A5) ,

(A6) ,

(A7) ,

(A8) ,

(A9) ,

(A10) ,

(A11) ,

(A12) ,

(A13) .

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

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

Функция  является коммутативной; элемент  играет роль нулевого элемента: , .

Операцию  определим следующими аксиомами:

(Р1) ,

(Р2) .

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

Операция  определяется следующим блоком аксиом:

(С1) ,

(С2) ,

(С3)

,

(С4) ,

(С5)

,

(С6) ,

(С7) ,

(С8) ,

(С9) .

Операция  определяется блоком аксиом:

(F1) ,

(F2) ,

(F3) ,

(F4) ,

(F5) ,

(F6) ,

(F7) .

Отметим, что формально аксиомы С8 и F4 не являются независимыми и могут быть выведены из аксиомы А6, однако для характеризации свойств операций и  их полезно выделить отдельно.

Введем также операции абстракции () и инкапсуляции (), где  – множество, параметризующее эти операции. Операции  и  определены на множестве  и имеют вид .

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

(AB1) ,

(AB2) ,

(AB3) ,

(AB4) ,

(AB5) ,

(AB6) ;

(E1) ,

(E2) ,

(E3) ,

(E4) ,

(E5) ,

(E6) .

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

(СН) Пусть  входит в  и . Тогда, если  получено из  путем замены  на , то .

Теорема 1. Формальная система, состоящая из блоков А1А13, P1P2, C1C9, F1F7 и правил вывода СН, непротиворечива.

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

Эквациональная характеризация семантических значений

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

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

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

Определение 9. Пусть  и  и . Частичные функции  и  определяются следующей таблицей:

Заметим, что для выражения  понятия префикса и суффикса не определяются, поскольку  (аксиома А12).

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

,    

где ,

,

где , , что , и , что .

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

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

Пример 2: .

В соответствии с семантическим определением имеем , где , .

,

где .

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

Аналогично предыдущему получаем

.

Таким образом, имеем .

Представим  в виде системы уравнений. Обозначим  через . Тогда

  +,

  =.

Далее получаем

,

,

,

,

.

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

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

,

,

Таким образом, выводим следующую систему уравнений:

,

,

.

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

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

Доказательство. Методом индукции по структуре P.

Базис. Для , где , эквациональная характеризация вытекает тривиально.

Индуктивный шаг. Пусть  и  будут эквационально характеризуемы. Тогда необходимо доказать, что  и  эквационально характеризуемы.

По предположению индукции существуют множества  и , такие, что и

1. . Обозначим

.

Запишем  вместо . Количество выражений (1) конечно. По индуктивному предположению имеем

.

Применяя аксиомы А4, А2, А5 и А11, получаем

.

Если , где , то применим еще раз аксиому А4, заменяя в  слагаемое  выражением , причем, если , то заменяем его представлением для  из .

Применяя далее аксиомы А1, А2, А3 и А5, получим

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

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

3. . Обозначим

                                            (2)

.

Запишем  вместо  и  вместо . Количество выражений (2) конечно. По индуктивному предположению имеем

Используя аксиомы А1, А2, А3, получим  , где все выражения и  входят в (2). Поскольку , получаем, что эквационально характеризуемо.

4. . Обозначим

                                            (3)

.

Запишем  вместо  и  вместо . Количество выражений (3) конечно. По индуктивному предположению имеем

.

Применяя аксиому Р1, а затем аксиомы , получим:

.

Если  и , то, применяя аксиомы С7, С9, А4, А5, а затем аксиомы , получим

где все  и  входят в (3). Поскольку , получаем, что  эквационально характеризуемо.

5.

.

Количество выражений (4) конечно. По индуктивному предположению имеем

.

Поскольку по определению имеем, что  есть минимальная фиксированная точка оператора , где

то, подставляя в оператор F(P1), имеем

Отсюда получаем следующее свойство для фиксированной точки  .

Используя это свойство, имеем , где .

Применяя аксиомы А4, А5 и А11, получим

+

        (5)

где все  входят в (4), а , поскольку  может принимать лишь одно из трех значений:  что соответствует определению .

Для  по индуктивному предположению имеем

Используя аксиомы А4, А5, А6, А8, А11, получаем

.

Рассмотрим последнее слагаемое .

Если сумма  содержит , то заменяем в соответствующем слагаемом выражение  его представлением (5).

Применяя вновь аксиому А4, получим

,

где все ,  входят в (4).

Таким образом, получаем, что  эквационально характеризуемо. Теорема полностью доказана.

Программная реализация

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

будут построены семантическое значение

и соответствующая система рекурсивных уравнений:

.

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

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

Литература

1.     Кораблин Ю.П. Семантика языков распределенного программирования. М.: Изд-во МЭИ, 1996. 102 с.

2.     Кораблин Ю.П. Семантика языков программирования. М.: Изд-во МЭИ, 1992. 102 с.