Кораблин Ю.П. (y.p.k@mail.ru) - Российский государственный социальный университет, г. Москва (профессор), Москва, Россия, доктор технических наук, Кучугуров И.В. (tws13@mail.ru) - Российский государственный социальный университет, г. Москва, Косакян М.Л. (xbix@list.ru) - Российский государственный социальный университет, г. Москва, Москва, Россия, Аспирант | |
Ключевые слова: разрешимость систем рекурсивных уравнений, эквивалентность, эквациональная характеризация, процессная семантика, верификация |
|
Keywords: solvability of system of recursive equations, equivalence, equational characterization, process semantics, verification |
|
|
При создании качественных программ важную роль играет этап верификации, в процессе которого возникает потребность анализа отдельных частей программы на наличие тупиков, блокировок, зацикливаний и т.д. Также возникает необходимость проверки программ на различные виды эквивалентности. При этом программе сопоставляется множество вычислительных последовательностей (путей). В [1] было показано, что множество вычислительных последовательностей (ВП)
где Определим метод сравнения систем рекурсивных уравнений вида Элементы множеств Заметим, что при внешнем сходстве этого преобразования с использованием аксиомы дистрибутивности Определим операции над множествами выражений и аксиоматизируем свойства операций над этими множествами. Пусть (S1) (S2) (S3)
Используя теперь в дополнение к ранее приведенным аксиомам формальной системы аксиомы построим алгоритм сравнения двух систем рекурсивных уравнений следующим образом. Пусть даны две системы рекурсивных уравнений для выражений
Применяя аксиомы S1 и S2 в сочетании со свойствами ассоциативности и коммутативности операции
где все Возможны следующие ситуации: а) б) в) Представленную выше процедуру выписывания уравнений продолжаем для получаемых пар 1. Построены две системы рекурсивных уравнений, эквивалентные с точностью до обозначений (на каждом шаге построения систем имела место только ситуация а)). В этом случае множество вычислительных последовательностей, задаваемых выражениями 2. Построены две системы рекурсивных уравнений, в процессе построения которых имели место лишь ситуации а) и б). В этом случае множество вычислительных последовательностей, определяемых выражением 3. При построении систем рекурсивных уравнений имела место ситуация в) либо ситуация б) применялась как в прямом, так и в инверсном виде, то есть, если при первоначальном появлении ситуации б) имеет место гипотеза о том, что множество ВП, определяемых выражением Продемонстрируем применение предложенного метода на следующем примере. Пример 1. Пусть
Выясним, эквивалентны ли значения
Полученные системы уравнений совпадают с точностью до обозначения переменных, а следовательно, значения Разрешимость систем рекурсивных уравнений Докажем, что множество ВП, характеризуемое системой уравнений Введем оператор
Оператор Обозначим через
то есть каждому множеству ВП
где
Запись Поскольку решение системы рекурсивных уравнений ассоциируется с Пример 2. Пусть дана система уравнений:
Тогда
Зададим несколько первых аппроксимаций решения этой системы:
где H Данное решение в точности совпадает с полученным ранее результатом. Для доказательства корректности задания априорной семантики необходимо показать, что решение системы рекурсивных уравнений Область для поиска решения систем рекурсивных уравнений вида (*) есть Для Прежде чем определить метрику на области S, приведем ряд определений и известных результатов из области метрических пространств. Определение 1. Метрика d на множестве Определение 2. Последовательность Определение 3. Последовательность Определение 4. Метрическое пространство Лемма 1. Метрическое пространство Определение 5 (Хаусдорфова мера). Пусть а) Метрика между б) Метрика между Теорема 1. Если Следствием этой теоремы является полнота метрического пространства ( Определим метрику на искомой области Определение 6. Пусть Лемма 2. Пространство Доказательство. Выберем Поскольку Последовательности Далее возьмем Лемма 3. Отображение Y метрического пространства Доказательство. Пусть Если Если Приписывание в конец последовательности элемента В соответствии с определением Очевидно, что для уменьшения значения функции меры Отсюда, в силу свойства оператора Доказанная лемма позволяет использовать следующее свойство отображений полных метрических пространств. Теорема 2 (теорема Банаха). Пусть 1) 2) Из этой теоремы с учетом вышеизложенного непосредственно следует искомый результат. Теорема 3. Оператор Таким образом, определенная выше семантика языка распределенного программирования является корректной. Эквивалентность схем распределенных программ в случае отсутствия побочного эффекта В [3] были рассмотрены методы доказательства эквивалентности схем программ. В частности, с использованием методов денотационной семантики доказана справедливость следующего утверждения: Оно может быть записано в базисном языке распределенного программирования следующим образом: Используя алгебраические методы данной главы, докажем справедливость утверждения
Обозначим
Представим теперь
Нетрудно заметить, что множество При первоначальном вычислении выражения Очевидно, что наличие побочного эффекта является нежелательной ситуацией. Поэтому целесообразно построение формализма, позволяющего осуществлять анализ программ, не допускающих побочного эффекта. Для этой цели следует переопределить ряд понятий, введенных ранее, и добавить аксиомы, характеризующие их свойства. Вначале расширим множество тестов Запись «…» означает все введенные ранее тесты. Новое множество тестов характеризуется следующим блоком аксиом: (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 |
http://swsys.ru/index.php?id=2915&lang=%E2%8C%A9%3Den&like=1&page=article |
|