Система Maude - это реализация логики перезаписи, разработанной в SRI International . Это похоже в общем подходе к Джозефу Гоген «s OBJ3 реализации эквациональной логики , но на основе переписывания логики , а не порядок отсортированных эквациональные логик , и с тяжелым акцентом на мощном метапрограммировании на основе отражения .
Maude - бесплатное программное обеспечение, а учебные пособия доступны в Интернете.
Элементарный пример
Модули Мод (теории перезаписи) состоят из терминологического языка плюс наборов уравнений и правил перезаписи. Термины в теории перезаписи конструируются с использованием операторов (функций, принимающих 0 или более аргументов какого-либо типа , которые возвращают термин определенного вида ). Операторы, принимающие 0 аргументов, считаются константами, и с помощью этих простых конструкций создается свой язык терминов.
Пример 1
fmod NAT есть сорт Нат. op 0: -> Nat [ctor]. op s: Nat -> Nat [ctor]. endfm
Эта теория перезаписи определяет все натуральные числа. Рода говоря, вводят, что существует своего рода под названием Nat (сокращенно натуральных чисел), и ниже приводится описание того , как построены эти термины. Оператор s в Примере 1 является функцией-преемником, представляющей следующее натуральное число в последовательности натуральных чисел, то есть s (N): = N + 1. s (0) предназначен для представления натурального числа 1 и так далее. 0 - константа, она не принимает никаких входных параметров, но возвращает Nat .
Пример 2
fmod NAT есть сорт Нат. op 0: -> Nat [ctor]. op s: Nat -> Nat [ctor]. op _ + _: Нат Нат -> Нат. vars NM: Nat. уравнение 0 + N = N. уравнение s (N) + M = s (N + M).endfm
В примере 2 вводится знак + , который обозначает сложение натуральных чисел. Его определение почти идентично предыдущему, с сортировкой ввода и вывода , но есть разница: его оператор имеет подчеркивания с каждой стороны. Мод позволяет пользователю указать, являются ли операторы инфиксными, постфиксными или префиксными (по умолчанию), это делается с использованием подчеркивания в качестве заполнителей места для вводимых терминов. Таким образом, оператор + принимает данные с каждой стороны, что делает его инфиксным. В отличие от нашего предыдущего оператора s, который принимает свои входные термины после оператора (префикса).
Три звездочки - это комментарии Мод к остальной части строки, которые позволяют синтаксическому анализатору знать, что он может игнорировать остальную часть строки (не часть программы), а круглые скобки означают комментарии раздела:
*** остальная часть строки игнорируется Мод*** (разделявляетсяигнорируется Мод)
Расширенный модуль Nat также содержит две переменные и два набора уравнений.
vars NM: Nat.уравнение 0 + N = N.уравнение s (N) + M = s (N + M).
Когда Мод «выполняет», он переписывает условия в соответствии с нашими требованиями. И это делается с помощью заявления
уменьшить в <некоторый модуль>: <некоторый термин>.
или более короткая форма
красный <какой-то термин>.
Для использования этого последнего утверждения важно, чтобы ничего не было двусмысленным. Небольшой пример из нашей теории перезаписи, представляющий натуральные числа:
уменьшить в NAT: s (0) + s (0).перезаписывает: 2 в ЦП 0 мс (реальная 0 мс) (~ перезаписей в секунду)результат Nat: s (s (0))
Используя два уравнения в теории перезаписи, NAT Мод сумел свести наш член к желаемому члену, представлению числа два, то есть второго преемника 0 . В этот момент никакое другое применение этих двух уравнений было невозможно, поэтому Мод останавливается. Мод переписывает члены в соответствии с уравнениями всякий раз, когда есть совпадение между закрытыми членами, которые пытаются переписать (или уменьшить), и левой частью уравнения в нашем наборе уравнений. В этом контексте совпадение - это замена переменных в левой части уравнения, которая оставляет его идентичным члену, который пытаются переписать / уменьшить.
Чтобы проиллюстрировать это далее, можно посмотреть на левую часть уравнений, когда Мод выполняет, сокращая / переписывая член.
уравнение s (N) + M = s (N + M).
может применяться к термину:
s (0) + s (0)
с момента замены:
N => 0M => s (0)s (N) + M [[N => 0, M => s (0)]] == s (0) + s (0)
делает их идентичными, и поэтому его можно уменьшить / переписать с помощью этого уравнения. После того, как это уравнение было применено к члену, остается термин:
s (0 + s (0))
Если внимательно взглянуть на этот термин, они увидят, что у него есть подходящая подстановка с соответствием первому уравнению, по крайней мере, часть члена соответствует первому уравнению:
уравнение 0 + N = N.
замена:
N => s (0)s (0 + N) [[N => s (0)]] == s (0 + s (0))0 + s (0) - соответствует первому уравнению и переписывается
На втором этапе замены и перезаписи внутренний член переписывается (весь член не соответствует ни одному из уравнений, но внутренний член соответствует). В итоге получается наш результирующий член s (s (0)) , и может показаться, что сложить 1 + 1 будет довольно сложно, но, надеюсь, вы скоро убедитесь в силе этого подхода.
Еще одна вещь, о которой стоит упомянуть, заключается в том, что сокращение / переписывание до этого момента принимало что-то очень важное как должное, а именно:
- Уменьшение / перезапись прекращается
- Уменьшение / перезапись вырожденная (применяя уравнения в любом порядке в конечном счете приведет к тому же в результате сроку)
Это не может считаться само собой разумеющимся, и для того, чтобы теория переписывания была разумной, нужно убедиться, что эквациональное приложение сливается и завершается. Доказать, что перезапись термов завершается, невозможно во всех случаях, что мы знаем из изучения проблемы остановки . Чтобы иметь возможность доказать, что перезапись термов (в отношении уравнений) прекращается, обычно можно создать некоторое отображение между термами и натуральными числами и показать, что применение уравнений уменьшает ассоциированное значение члена. Затем индукция доказывает, что это останавливающий процесс, поскольку событие нахождения меньших натуральных чисел - это останавливающий процесс. Естественно, наборы уравнений, которые могут привести к тому, что перезапись терма будет содержать циклы, не будут завершаться. Доказательство слияния - еще один важный аспект, поскольку теория перезаписи, лишенная этой способности, будет довольно ошибочной. Чтобы доказать, что набор уравнений конфлюэнтен, необходимо доказать, что любое применение уравнений к любому члену принадлежности приведет к одному и тому же результирующему члену (завершение - предварительное условие). Подробности о том, как доказать завершение или слияние, здесь не приводится, это просто нужно упомянуть, поскольку именно здесь уравнения и правила перезаписи различаются, что является следующей темой этого краткого обзора.
Правила перезаписи
До этого момента переписывание и сокращение были более или менее одинаковыми вещами, наша первая теория перезаписи не имела правил перезаписи, но мы все же переписали термины, так что пришло время проиллюстрировать, что такое правила перезаписи, и чем они отличаются от уравнений, которые у нас есть. мы видели до сих пор (они не сильно отличаются от уравнений, естественно, поскольку мы говорим об этих двух концепциях почти как взаимозаменяемые).
Представленный до сих пор модуль NAT, который представлял натуральные числа и сложение его элементов, считается функциональным модулем / теорией перезаписи, поскольку он не содержит правил перезаписи. Такие модули часто инкапсулирует с FMOD и endfm (вместо мод ENDM ) , чтобы проиллюстрировать этот факт. Функциональный модуль и его набор уравнений должны быть сливающимися и завершающимися, поскольку они составляют часть теории перезаписи, которая всегда должна вычислять один и тот же результат, это станет ясно, когда правила перезаписи войдут в игру.
Пример 3
мод PERSON естьвключая NAT. *** наш предыдущий модульСортировка Person.Состояние сортировки.оп замужем: -> Государственный [ctor].оп развелась: -> гос [ctor].op single: -> State [ctor].op задействован: -> State [ctor].op dead: -> Состояние [ctor].op person: State Nat -> Person [ctor].var N: Nat.var S: Состояние.rl [день рождения]:человек (S, N) => человек (S, N + s (0)).rl [обручиться]:person (single, N) => человек (помолвлен, N).рл [жениться]:person (помолвлен, N) => человек (женат, N).рл [разводиться]:person (женат, N) => человек (разведен, N).rl [лас-вегас]:person (S, N) => человек (женат, N).rl [умереть]:person (S, N) => человек (мертвый, N).конец
Этот модуль представляет два новых сорта , и набор правил перезаписи. Мы также включаем наш предыдущий модуль, чтобы проиллюстрировать, чем отличаются уравнения и правила перезаписи. Правила перезаписи рассматриваются как набор юридических изменений состояния, поэтому, хотя уравнения имеют одно и то же значение по обе стороны от знака равенства, правила перезаписи - нет (в правилах перезаписи используется знак => вместо знака равенства). После свадьбы вы все тот же человек (это открыто для обсуждения), но что-то изменилось, по крайней мере, ваше семейное положение. Это иллюстрируется правилом перезаписи, а не уравнением. Правила перезаписи не обязательно должны сливаться и завершаться, поэтому очень важно, какие правила будут выбраны для перезаписи термина. Правила применяются «случайным образом» системой Мод, что означает, что вы не можете быть уверены, что одно правило применяется перед другим правилом и так далее. Если к термину можно применить уравнение, оно всегда будет применяться перед любым правилом перезаписи.
Небольшой пример:
Пример 4
перепишите [3] в PERSON: person (single, 0).перезаписывает: 4 в ЦП 0 мс (реальная 0 мс) (~ перезаписывает / сек)результат Человек: человек (женат, s (0))
Здесь мы говорим системе Мод переписать наш входной член в соответствии с теорией перезаписи, и мы приказываем ей остановиться после 3 шагов перезаписи (помните, что правила перезаписи не обязательно должны завершаться или сливаться, поэтому верхняя граница - неплохая идея) , мы просто хотим увидеть, в каком состоянии мы окажемся после случайного выбора 3 правил соответствия . И, как видите, состояние, в котором оказывается этот человек, может показаться немного странным. (Когда ты замужем в возрасте одного года, я думаю, что в детском саду ты немного выделяешься). В нем также говорится, что 4 шага перезаписи, хотя мы специально указали верхний предел в 3 шага перезаписи, это потому, что шаги перезаписи, которые являются результатом применения уравнений, не учитываются (они не меняют термин, по крайней мере, если уравнения разумны) . В этом примере одно из уравнений модуля NAT использовалось для уменьшения члена 0 + s (0) до s (0) , что составляет 4-й шаг перезаписи.
Чтобы сделать эту теорию перезаписи немного менее болезненной, мы можем немного изменить некоторые из наших правил перезаписи и сделать их условными правилами перезаписи, что в основном означает, что они должны соответствовать некоторым критериям, которые будут применяться к термину (кроме простого соответствия левой сторона правила перезаписи).
crl [лас-вегас]:person (S, N) => person (женат, N) if (S = / = женат) / \ (S = / = мертв).crl [умереть]:person (S, N) => person (мертвый, N), если (S = / = мертвый).
Кажется разумным, что вы не можете умереть после смерти и не можете жениться, пока состоите в браке. Предполагается, что наклонные зубочистки ( / \ ) напоминают логическое И, что означает, что для применения правила должны быть выполнены оба критерия (кроме сопоставления терминов). Аналогичным образом можно сделать условными уравнения .
Зачем переписывать логику?
Мод намеревается решать набор проблем, отличный от обычных императивных языков, таких как C, Java или Perl. Это формальный инструмент рассуждения, который может помочь нам убедиться, что все идет «так, как должно», и показать нам, почему это не так, если это так. Другими словами, Мод позволяет нам формально определить, что мы подразумеваем под некоторым понятием, в очень абстрактной манере (не касаясь того, как внутренне представлена структура и т. Д.), Но мы можем описать то, что считается равным в нашей теории. ( уравнения ) и через какие изменения состояния он может пройти ( правила перезаписи ). Это чрезвычайно полезно для проверки протоколов безопасности и критического кода. Система Maude доказала недостатки в протоколах криптографии, просто указав, что система может делать (аналогично теории перезаписи PERSON), и путем поиска нежелательных ситуаций (состояний или условий, которые не должны быть достижимы) протокол может будет показано, что в нем есть ошибки, а не ошибки программирования, но случаются ситуации, которые трудно предсказать, просто идя по «счастливому пути», как это делает большинство разработчиков.
Мы можем использовать встроенный поиск Мод, чтобы искать нежелательные состояния, или его можно использовать, чтобы показать, что такие состояния не могут быть достигнуты.
Еще раз небольшой пример из нашего модуля ПЕРСОНА.
поиск [1] в PERSON: человек (холост, 1) => 1 человек (женат, 2).Нет решения.
Здесь натуральные числа имеют более привычный вид (загружены базовые модули Maude prelude.maude, это можно сделать с помощью команды « in prelude », либо 1 можно заменить на s (0), а 2 - на s (s ( 0)), если вы не хотите загружать модули Мод по умолчанию), естественно, Мод имеет встроенную поддержку обычных структур, таких как целые числа, числа с плавающей запятой и так далее. Натуральные числа по-прежнему являются членами встроенной сортировки Nat. Мы заявляем, что хотим найти переход, используя одно правило перезаписи (=> 1), которое перезаписывает первый член в другой. Результат расследования не шокирует, но все же иногда доказывать очевидное - это все, что мы можем сделать. Если мы позволим Мод использовать более одного шага, мы увидим другой результат:
поиск [1] в PERSON: человек (холост, 1) => + человек (женат, 2).Решение 1 (состояние 7)состояния: 8 перезаписей: 14 в ЦП 0 мс (реальная 0 мс) (~ перезаписей в секунду)
Чтобы увидеть, что привело нас в этом направлении, мы можем использовать встроенную команду show path, которая позволяет нам узнать, какие приложения правил привели нас к полученному термину. Маркер (=> +) означает применение одного или нескольких правил.
показать путь 7.состояние 0, Человек: человек (одинокий, 1)=== [[rl person (S, N) => person (S, N + 1) [label 'birthday]].]===>состояние 1, Человек: человек (холост, 2)=== [[crl person (S, N) => person (женат, N), если S = / = женат = true / \ S = / = dead = true [label las-vegas]].]===>состояние 7, Лицо: человек (женат, 2)
Как мы видим, применение правила «день рождения», за которым следует «лас-вегас», привело нас туда, куда мы хотели. Поскольку все теории перезаписи или модули с множеством возможных приложений правил будут генерировать огромное дерево возможных состояний для поиска с помощью команды поиска , этот подход не всегда является решением. У нас также есть возможность контролировать, какие приложения правил следует пытаться использовать на каждом этапе, с помощью метапрограммирования из-за свойства отражения или логики перезаписи.
Рекомендации
- Клавел, Дюран, Екер, Линкольн, Марти-Oliet, Meseguer и Кесада, 1998. Мод как метаязык , в Proc. 2-й международный семинар по переписыванию логики и ее приложений, Электронные заметки в теоретической информатике 15, Эльзевир.
- Марти-Олиет и Хосе Месегер , 2002. Переписывая логику: дорожная карта и библиография . Теоретическая информатика 285 (2): 121-154.
- Марти-Олиет и Хосе Месегер , 1993–2000 годы. Переписывая логику как логико-семантическую структуру . Электронные заметки по теоретической информатике 4, Elsevier.
дальнейшее чтение
- Клавель, Дуран, Экер, Линкольн, Марти-Олиет, Месегер и Талкотт (2007). Все о моде - высокопроизводительная логическая структура: как определять, программировать и проверять системы в переписывании логики . Springer. ISBN 978-3-540-71940-3.CS1 maint: несколько имен: список авторов ( ссылка )
Внешние ссылки
- Домашняя страница Мод в Университете Иллинойса в Урбана-Шампейн;
- Домашняя страница Maude Tool в реальном времени, разработанная Питером Чаба Олвецки;
- Введение в Мод Нила Хармана, Университет Суонси ( исправленные ошибки )
- Распределенная архитектура на основе политик и целей, написанная SRI International на языке Maude.
- Maude для Windows , установщик Maude для Windows и Maude Development Tools , плагин Maude Eclipse, разработанный в рамках проекта MOMENT в Техническом университете Валенсии (Испания).