モードシステム

Maudeシステムは書き換え論理の実装です。Joseph GoguenによるOBJ3の等式論理実装と基本的なアプローチは似ていますが、順序ソート等式論理ではなく書き換え論理を基盤としており、リフレクションに基づく強力なメタプログラミングを重視しています。

Maudeはフリーソフトウェアであり、チュートリアルはオンラインで公開されています。元々はSRI International [ ¹^]で開発されましたが、現在は多様な研究者の協力によって開発されています^。^[²^]

導入

Maudeは、 C、Java、Perlといった通常の命令型言語とは異なる一連の問題を解決しようとします。Maudeは形式推論ツールであり、物事が「あるべき姿」にあるかどうかを検証し、そうでない場合はなぜそうではないのかを示すのに役立ちます。言い換えれば、Maudeは、ある概念が何を意味するのかを非常に抽象的な方法で形式的に定義することを可能にします（構造が内部的にどのように表現されているかなどには関わらず）。しかし、理論に関して等価と考えられるもの（方程式）と、それがどのような状態変化を経るか（書き換え規則）を記述することができます。

Maudeモジュール（書き換え理論）は、項言語と方程式および書き換え規則の集合から構成されます。書き換え理論の項は、演算子（0個以上の引数を取り、特定の種類の項を返す関数）を用いて構築されます。引数を取らない演算子は定数とみなされ、これらの単純な構成を用いて項言語を構築します。Maudeでは、演算子が中置、後置、または前置（デフォルト）のいずれであるかをユーザーが指定できます。これは、入力項の挿入句としてアンダースコアを使用することで行われます。

簡約方程式は合流かつ終了すると仮定されます。書き換え規則にはこの制限はありません。

Maude が「実行」すると、方程式と書き換え規則に従って項を書き換えます。Maude は、書き換え（または簡約）しようとする閉じた項と方程式セット内の方程式の左辺が一致する場合、常に方程式に従って項を書き換えます。ここでの「一致」とは、方程式の左辺の変数を置き換え、書き換え/簡約しようとする項と同一の状態にすることです。方程式と書き換え規則は条件付き規則になることもあり、つまり、項に適用するにはいくつかの基準を満たす必要があります（書き換え規則の左辺が一致するという条件だけでなく）。

ルールはMaudeシステムによって「ランダム」に適用されます。つまり、あるルールが別のルールよりも先に適用される、といったことは保証されません。項に方程式を適用できる場合、それは常にどの書き換えルールよりも前に適用されます。Maudeに組み込まれた検索機能は、不要な状態を探し出し、そのような状態には到達できないことを示します。Maudeは、リフレクティブプロパティまたは書き換えロジックにより、メタプログラミングを用いて各ステップでどのルール適用を試みるかを制御する機能を備えています。

使用法

Maudeは、セキュリティプロトコルや重要なコードの検証に使用されてきました。Maudeシステムは、システムが実行可能な動作を規定するだけで暗号プロトコルの欠陥を証明し、望ましくない状況（本来到達すべきではない状態や条件）を探すことで、プロトコルにバグが含まれていることを示しました。これはプログラミング上のバグではなく、多くの開発者が行う「ハッピーパス」を辿るだけでは予測が難しい状況が発生することを意味します。

参考文献

^ 「The Maude System:About」 . The Maude System . 2021年8月27日閲覧。
^ 「The Maude Project and Team」 . The Maude System . 2021年8月27日閲覧。

さらに読む

Clavel、Durán、Eker、Lincoln、Martí-Oliet、Meseguer、Quesada、1998 年、「メタ言語としての Maude」、Proc. 2nd International Workshop on Rewriting Logic and its Applications、Electronic Notes in Theoretical Computer Science 15、Elsevier。
Martí-OlietとJosé Meseguer、2002年。「論理の書き換え：ロードマップと参考文献」理論計算機科学285(2):121-154。
Martí-OlietとJosé Meseguer、1993-2000年。論理的かつ意味論的枠組みとしての論理の書き換え。理論計算機科学電子ノート4、Elsevier。
Clavel, Durán, Eker, Lincoln, Martí-Oliet, Meseguer, Talcott (2007). All About Maude - 高性能論理フレームワーク：書き換えロジックにおけるシステムの仕様定義、プログラミング、検証の方法(PDF) . Springer. ISBN 978-3-540-71940-3。{{cite book}}: CS1 maint: 複数の名前: 著者リスト (リンク)

外部リンク

イリノイ大学アーバナシャンペーン校のMaude ホームページ。
Peter Csaba Ölveczky が開発したReal-Time Maude Tool のホームページ。
スウォンジー大学のニール・ハーマンによるモード入門（訂正あり）
SRI International が Maude で書いたポリシーと目標に基づく分散アーキテクチャ。
Windows 用のMaude インストーラーである Maude for Windows と、スペインのバレンシア工科大学のMOMENT プロジェクトによって開発された Maude Eclipse プラグインであるMaude Development Toolsです。

[1] 「The Maude System:About」 . The Maude System . 2021年8月27日閲覧。

[2] 「The Maude Project and Team」 . The Maude System . 2021年8月27日閲覧。

1

。