Система Мод - Maude system

В Система Мод это реализация переписывание логики разработан в SRI International. По своему общему подходу он похож на Джозеф Гогуэн с 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 является константой, не принимает никаких входных параметров, но возвращает Нат.

Пример 2

fmod NAT - это вроде Нат. op 0: -> Nat [ctor]. op s: Nat -> Nat [ctor]. op _ + _: Нат Нат -> Нат. vars N M: Нат. уравнение 0 + N = N. уравнение s (N) + M = s (N + M) .endfm

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

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

*** остальная часть строки игнорируется Мод *** (раздел игнорируется Мод)

Расширенный Нат модуль также содержит две переменные и два набора уравнений.

vars N M: Nat. экв 0 + N = N. экв s (N) + M = s (N + M).

Когда Мод «выполняет», он переписывает условия в соответствии с нашими требованиями. И это делается с помощью заявления

уменьшить в <некоторый модуль>: <некоторый термин>.

или более короткая форма

красный <какой-то термин>.

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

уменьшить в NAT: s (0) + s (0) .rewrites: 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 (вместо мод конец), чтобы проиллюстрировать этот факт. Функциональный модуль и его набор уравнений должны сливаться и завершаться, поскольку они составляют часть теории перезаписи, которая всегда должна вычислять один и тот же результат, это станет ясно, когда правила перезаписи войдут в игру.

Пример 3

мод PERSON включает NAT. *** наш предыдущий модуль: Сортировка Человек. Сортировать Состояние .op женат: -> Состояние [ctor] .op разведено: -> Состояние [ctor] .op не замужем: -> Состояние [ctor] .op занято: -> Состояние [ctor] .op dead: -> State [ctor] .op person: State Nat -> Person [ctor] .var N: Nat .var S: состояние .rl [день рождения]: person (S, N) => person (S, N + s (0)) .rl [обручиться]: человек (холост, N) => человек (помолвлен, N) .rl [жениться]: человек (помолвлен, N) => человек (женат, N ) .rl [разводиться]: человек (женат, N) => человек (разведен, N) .rl [лас-вегас]: человек (S, N) => человек (женат, N) .rl [умереть] : person (S, N) => person (мертв, N) .endm

В этом модуле представлены два новых сортирует, и набор правил перезаписи. Мы также включаем наш предыдущий модуль, чтобы проиллюстрировать, чем отличаются уравнения и правила перезаписи. Правила перезаписи рассматриваются как набор юридических изменений состояния, поэтому, хотя уравнения имеют одно и то же значение с обеих сторон знака равенства, правила перезаписи - нет (в правилах перезаписи используется знак => вместо знака равенства). После свадьбы вы все тот же человек (это открыто для обсуждения), но что-то изменилось, по крайней мере, ваше семейное положение. Так что это иллюстрируется правилом перезаписи, а не уравнением. Правила перезаписи делают нет должен быть сливаться и прекращение так что очень важно, какие правила были выбраны для переписывания термина. Правила применяются «случайным образом» системой Мод, что означает, что вы не можете быть уверены, что одно правило применяется перед другим правилом и так далее. Если уравнение может быть применено к члену, это будет всегда применяться перед любое правило перезаписи.

Небольшой пример:

Пример 4

rewrite [3] в PERSON: person (single, 0) .rewrites: 4 in 0ms cpu (0ms real) (~ rewrites / second) result Person: person (женат, s (0))

Здесь мы говорим системе Maude переписать наш входной член в соответствии с теорией перезаписи, и мы приказываем ей остановиться после 3 шагов перезаписи (помните, что правила перезаписи не обязательно должны завершаться или сливаться, поэтому верхняя граница - неплохая идея) , мы просто хотим увидеть, в каком состоянии мы окажемся после случайного выбора 3 соответствие правила. И, как видите, состояние, в котором оказывается этот человек, может показаться немного странным. (Когда вы выходите замуж в возрасте одного года, я думаю, вы немного выделяетесь в детском саду). В нем также говорится, что 4 шага перезаписи, хотя мы специально указали верхний предел в 3 шага перезаписи, это потому, что шаги перезаписи, которые являются результатом применения уравнений, не учитываются (они не меняют термин, по крайней мере, если уравнения разумны) . В этом примере одно из уравнений модуля NAT было использовано для сокращения члена 0 + с (0) к s (0), что составляет 4-й шаг перезаписи.

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

crl [las-vegas]: person (S, N) => person (женат, N) if (S = / = женат) /  (S = / = мертв) .crl [die]: person (S, N) => человек (мертв, N), если (S = / = мертв).

Кажется разумным, что вы не можете умереть после смерти и не можете жениться, пока состоите в браке. Опирающиеся зубочистки (/\) должны напоминать логический И это означает, что для применения правила должны быть выполнены оба критерия (кроме сопоставления терминов). Уравнения аналогичным образом можно сделать условным.

Зачем переписывать логику?

Мод намеревается решать набор проблем, отличный от обычных императивных языков, таких как C, Java или Perl. Это формальный инструмент рассуждения, который может помочь нам убедиться, что все обстоит «так, как должно», и показать нам, почему это не так, если это так. Другими словами, Мод позволяет нам формально определить, что мы подразумеваем под некоторым понятием, в очень абстрактной манере (не касаясь того, как структура внутренне представлена ​​и т. Д.), Но мы можем описать то, что считается равным в нашей теории. (уравнения) и через какие изменения состояния он может пройти (переписать правила). Это чрезвычайно полезно для проверки протоколов безопасности и критического кода. Система Maude доказала недостатки в протоколах криптографии, просто указав, что система может делать (аналогично теории перезаписи PERSON), и путем поиска нежелательных ситуаций (состояний или условий, которые не должны быть достижимы) протокол может будет показано, что в нем есть ошибки, а не ошибки программирования, но случаются ситуации, которые трудно предсказать, просто идя по «счастливому пути», как это делает большинство разработчиков.

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

Еще раз небольшой пример из нашего модуля ПЕРСОНА.

поиск [1] ​​в ЛИЦО: человек (холост, 1) => 1 человек (женат, 2). Нет решения.

Здесь натуральные числа имеют более привычный вид (загружены базовые модули Maude prelude.maude, это можно сделать с помощью команды "в прелюдии", или 1 можно заменить на s (0) и 2 на s (s (0)), если вы не хотите загружать модули Мод по умолчанию), естественно, Мод имеет встроенную поддержку обычных структур, таких как целые числа и с плавающей точкой и т. д. Натуральные числа по-прежнему являются членами встроенной Сортировать Nat. Мы заявляем, что хотим найти переход, используя одно правило перезаписи (=> 1), которое перезаписывает первый член в другой. Результат расследования не является шокирующим, но все же иногда доказывать очевидное - это все, что мы можем сделать. Если мы позволим Мод использовать более одного шага, мы увидим другой результат:

поиск [1] ​​в PERSON: person (single, 1) => + person (женат, 2). Решение 1 (состояние 7) гласит: 8 перезаписей: 14 в ЦП с 0 мс (реальное значение 0 мс) (~ перезаписей в секунду)

Чтобы увидеть, что привело нас в этом направлении, мы можем использовать встроенную команду показать путь что позволяет нам узнать, какие применения правил привели нас к полученному термину. Маркер (=> +) означает применение одного или нескольких правил.

показать путь 7. состояние 0, Человек: person (single, 1) === [[rl person (S, N) => person (S, N + 1) [label 'birthday]].] ===> состояние 1, Человек: человек (холост, 2) === [[crl person (S, N) => человек (женат, N), если S = ​​/ = женат = правда /  S = / = мертв = верно [label las -vegas]].] ===> состояние 7, Человек: человек (женат, 2)

Как мы видим, применение правила «день рождения», за которым следует «лас-вегас», привело нас туда, куда мы хотели. Поскольку все теории переписывания или модули со множеством возможных приложений правил будут генерировать огромное дерево возможных состояний для поиска с помощью поиск командование, такой подход не всегда является решением. У нас также есть возможность контролировать, какие приложения правил должны выполняться на каждом этапе, используя метапрограммирование из-за отражающего свойства или логики перезаписи.

Рекомендации

дальнейшее чтение

  • Клавель, Дуран, Экер, Линкольн, Марти-Олиет, Месегер и Талкотт (2007). Все о моде - высокопроизводительная логическая структура: как определять, программировать и проверять системы в переписывании логики. Springer. ISBN  978-3-540-71940-3.CS1 maint: несколько имен: список авторов (связь)

внешняя ссылка