Система Maude представляет собой реализацию логики переписывания . Она похожа по своему общему подходу на реализацию эквациональной логики OBJ3 Джозефа Гогена , но основана на логике переписывания, а не на упорядоченной эквациональной логике, и с сильным акцентом на мощном метапрограммировании, основанном на рефлексии .
Maude — это бесплатное программное обеспечение, и обучающие материалы доступны онлайн. Первоначально он был разработан в SRI International , [1] , но теперь разрабатывается разнообразным сотрудничеством исследователей. [2]
Maude решает другой набор проблем, чем обычные императивные языки, такие как C , Java или Perl . Это формальный инструмент рассуждения, который может помочь нам проверить, что все "так, как должно быть", и показать нам, почему это не так, если это так. Другими словами, Maude позволяет нам формально определить, что мы подразумеваем под некоторой концепцией, очень абстрактным образом (не касаясь того, как структура представлена внутри и т. д.), но мы можем описать то, что считается равным относительно нашей теории ( уравнения ) и какие изменения состояния она может пройти ( правила переписывания ).
Модули Maude (теории перезаписи) состоят из термин-языка плюс наборы уравнений и правил перезаписи. Термины в теории перезаписи строятся с использованием операторов (функций, принимающих 0 или более аргументов некоторого вида , которые возвращают термин определенного вида). Операторы, принимающие 0 аргументов, считаются константами, и их термин-язык строится с помощью этих простых конструкций. Maude позволяет пользователю указывать, являются ли операторы инфиксными, постфиксными или префиксными (по умолчанию), это делается с использованием подчеркиваний в качестве заполнителей для входных терминов.
Предполагается, что уравнения редукции являются конфлюэнтными и завершающимися . Правила переписывания не имеют этого ограничения.
Когда Maude «выполняется», он переписывает термины в соответствии с уравнениями и правилами перезаписи. Maude переписывает термины в соответствии с уравнениями всякий раз, когда есть совпадение между закрытыми терминами , которые пытаются переписать (или сократить), и левой частью уравнения в нашем наборе уравнений. Соответствие в этом контексте — это замена переменных в левой части уравнения, которая оставляет его идентичным термину, который пытаются переписать/сократить. Уравнения и правила перезаписи также могут быть условными правилами, что означает, что они должны соответствовать некоторым критериям, чтобы быть примененными к термину (помимо простого соответствия левой части правила перезаписи).
Правила применяются системой Maude «случайно», что означает, что вы не можете быть уверены, что одно правило применяется раньше другого и т. д. Если уравнение может быть применено к термину, оно всегда будет применено до любого правила перезаписи. Встроенный поиск Maude может искать нежелательные состояния и показывать, что такие состояния не могут быть достигнуты. Maude имеет возможность контролировать, какие приложения правил должны быть предприняты на каждом шаге, используя метапрограммирование , благодаря свойству рефлексии или логике перезаписи.
Maude использовался для проверки протоколов безопасности и критического кода. Система Maude доказала недостатки в протоколах криптографии, просто указав, что может делать система, и выявив нежелательные ситуации (состояния или условия, которые не должны быть достижимы), можно показать, что протокол содержит ошибки, не ошибки программирования, а ситуации, которые трудно предсказать, просто следуя по «счастливому пути», как это делают большинство разработчиков.
{{cite book}}: CS1 maint: multiple names: authors list (link)