Система Мод

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

Maude — бесплатное программное обеспечение, учебные пособия доступны в Интернете. Первоначально он был разработан в SRI International , но в настоящее время разработан в результате сотрудничества различных исследователей.

Введение

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

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

Уравнения редукции предполагаются вытекающими и обрывающимися . Правила перезаписи не имеют этого ограничения.

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

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

Использование

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

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

• Клавель, Дуран, Экер, Линкольн, Марти-Олиет, Месегер и Кесада, 1998. Мод как метаязык , в Proc. 2-й международный семинар по переписыванию логики и ее приложениям, Электронные заметки по теоретической информатике 15, Elsevier.
• Марти-Олиет и Хосе Месегер , 2002. Переписывание логики: дорожная карта и библиография . Теоретическая информатика 285(2):121-154.
• Марти-Олиет и Хосе Месегер , 1993–2000 гг. Переписывание логики как логической и семантической структуры . Электронные заметки по теоретической информатике 4, Elsevier.
• Клавель, Дюран, Экер, Линкольн, Марти-Олиет, Месегер и Талкотт (2007). Все о Мод - Высокопроизводительная логическая структура: как определять, программировать и проверять системы при переписывании логики (PDF) . Спрингер. ISBN  978-3-540-71940-3 . {{cite book}}: CS1 maint: несколько имен: список авторов ( ссылка )

Внешние ссылки

• Домашняя страница Мод в Университете Иллинойса в Урбана-Шампейн;
• Домашняя страница Real-Time Maude Tool , разработанная Питером Чабой Ольвечки;
• Введение в Мод Нила Хармана, Университет Суонси ( ошибки )
• Распределенная архитектура, основанная на политике и целях, написанная на языке Maude компанией SRI International.
• Maude для Windows , установщик Maude для Windows, и Maude Development Tools , плагин Maude Eclipse, разработанный в рамках проекта MOMENT в Техническом университете Валенсии (Испания).