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

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

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

,    

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

Определим метод сравнения систем рекурсивных уравнений вида , что позволит получить формальный метод для сравнения схем программ в языке . Очевидно, что наличие одинаковых префиксов в рекурсивных уравнениях приводит к необходимости сравнения не пар выражений , как это имело место в [2], а пар множеств выражений, имеющих одинаковые префиксы. Пусть даны две системы рекурсивных уравне- ний вида ; , которые исследуются на эквивалентность. В этих системах заданы рекурсивные уравнения для выражений  и  соответственно. Обозначим через  множество выражений , через , через  и  – множества всех подмножеств  и  соответственно.

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

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

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

(S1) ,

(S2) ,

(S3) 

.

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

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

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

,

.

Применяя аксиомы S1 и S2 в сочетании со свойствами ассоциативности и коммутативности операции , приводим уравнения для  к виду

,

,

где все  попарно различны, а  и .

Возможны следующие ситуации:

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

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

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

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

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

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

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

Продемонстрируем применение предложенного метода на следующем примере.

Пример 1. Пусть  и  – семантические значения, задаваемые системами уравнений , где , и , где

Выясним, эквивалентны ли значения  и .

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

Разрешимость систем рекурсивных уравнений

Докажем, что множество ВП, характеризуемое системой уравнений , задано корректно, то есть решение системы рекурсивных уравнений  существует.

Введем оператор

.

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

Обозначим через  пустое множество ВП либо кортеж из n пустых множеств ВП. Тогда имеем , то есть значению  соответствует кортеж :

,

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

  + 

  +,

где  и ;

  + 

  +.

Запись  означает взятие l-й проекции n, получаемой в результате i применений оператора  к n .

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

Пример 2. Пусть дана система уравнений:

,

,

,

,

,

,

.

Тогда

.

Зададим несколько первых аппроксимаций решения этой системы:

;

+  

;

+

;

 – фиксированная точка;

+

+

+

,

где H.

Данное решение в точности совпадает с полученным ранее результатом.

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

Область для поиска решения систем рекурсивных уравнений вида (*) есть , то есть S является декартовым произведением областей , где  – подмножество множества , содержащее конечные и бесконечные ВП вида , либо , либо ,  и .

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

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

Определение 1. Метрика d на множестве  определяется следующим образом:

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

Определение 3. Последовательность  точек метрического пространства сходится к точке x, если .

Определение 4. Метрическое пространство  называется полным, если в нем сходится любая фундаментальная последовательность.

Лемма 1. Метрическое пространство , где  задается в определении 1, является полным.

Определение 5 (Хаусдорфова мера). Пусть  – метрическое пространство.

а) Метрика между  и  определяется следующим образом: .

б) Метрика между  определяется как .

Теорема 1. Если  – полное метрическое пространство, то пространство  также является полным. Кроме того, любая фундаментальная последовательность  в  имеет предел: .

Следствием этой теоремы является полнота метрического пространства (, где  – Хаусдорфова мера.

Определим метрику на искомой области .

Определение 6. Пусть . Тогда  где  – проекции  на l-й компонент множества .

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

Доказательство. Выберем . Определим такое , что  для всех .

Поскольку  – фундаментальная последовательность, то , такое, что "i, j> Докажем, что для выбранного таким образом  утверждение  справедливо для всех

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

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

Лемма 3. Отображение Y метрического пространства  в себя является сжимающим отображением.

Доказательство. Пусть  и  – аппроксимации множеств ВП, получаемые в результате применения оператора Y к кортежу пустых множеств  некоторое количество раз. Определим  и  для некоторых  и  Требуется показать, что   .

Если , то это неравенство справедливо, так как в этом случае  и, следовательно, .

Если , то возьмем для определенности . Применение оператора  к  не уменьшает длину каждой ВП , где , так как к каждой незавершенной последовательности, принадлежащей , будет приписан либо элемент , либо элемент , либо элемент из .

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

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

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

Отсюда, в силу свойства оператора , увеличивающего длину каждой незавершенной последовательности, следует, что  для некоторого , а следовательно,  является сжимающим отображением метрического пространства

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

Теорема 2 (теорема Банаха). Пусть  – полное метрическое пространство и  – сжимающее отображение, то есть  Тогда существует  такое, что справедливо

1)  ( – фиксированная точка );

2)  ( – единственная фиксированная точка).

Из этой теоремы с учетом вышеизложенного непосредственно следует искомый результат.

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

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

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

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

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

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

.

Обозначим  через , а  через ;

,

.

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

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

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

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

Вначале расширим множество тестов , добавив в него отрицание и сложные тесты,  

Запись «…» означает все введенные ранее тесты. Новое множество тестов характеризуется следующим блоком аксиом:

(G1) ,

(G2) ,

(G3) F,

(G4) ,

(G5) ,

(G6) ,

(G7) ,

(G8) .

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

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

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

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

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

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

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

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

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

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

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

Литература

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

2.     Korablin Yu.P. Deciding equivalence of functional schemes for parallel programs // Mathematical Centre, Department of Computer Science, Reseach Report IW 200/82, Amsterdam, 1982.

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