maude bindings

Maude 的語言綁定

使用 SWIG 的 Maude 規範語言的語言綁定。他們利用 Maude 的修改版本，擴展了由策略控制的系統的模型檢查器，也可以透過綁定進行存取。

Python 套件可在 PyPI 上取得。使用pip install maude安裝後，可以直接使用，因為 Maude 已嵌入到套件中：

 import maude
maude . init ()
nat = maude . getModule ( 'NAT' )
t = nat . parseTerm ( '1 + 2' )
t . reduce ()
print ( t )

SWIG 支援的其他語言的綁定可以從此儲存庫構建，但尚未給予它們特定的支援和測試。其中一些的具體說明可在此處找到。

大樓

此儲存庫包含 Maude 的擴充版本作為子模組，必須先使用git submodule update --init或等效的 Git 指令來複製它。要建立 Python 包，可以透過任何標準命令使用 scikit-build-core：

 python -m build  # or
pip wheel .

這將導致 Maude 在subprojects目錄中構建，需要 Meson 建置系統、Ninja 以及各種外部程式庫和工具，如其儲存庫中所述。或者，可以從其發布部分下載 Maude 作為庫的編譯版本並將其放置在預期位置：

• subprojects/maudesmc/installdir/lib用於庫，以及
• subprojects/maudesmc/build為config.h頭檔。

在這種情況下或直接從其子目錄建立 Maude 時，應在上一個命令之前添加CMAKE_ARGS="-DBUILD_LIBMAUDE=OFF" 。

其他語言的綁定也可以直接使用 CMake 構建，其中srcdir是克隆存儲庫的目錄， language是 SWIG 支援的語言之一：

 cmake <srcdir> -DLANGUAGE=<language>
cmake --build .

對於某些語言目標來說，這已經足夠了，但對於其他語言目標，可能需要額外的步驟。

文件

此處提供了 Python 套件的文檔，這些文檔在很大程度上可以推廣到其他目標語言。 Javadoc 產生的文件也可用。除此之外，儲存庫中的範例可以用作各種主題的參考：

• 載入文件、解析術語、歸約、重寫、策略重寫以及在test.py中搜尋。
• 在match.py​​ 中進行匹配。
• 在apply.py中選擇性地應用規則。
• 統一在unify.py中。
• 在graph.py中操作重寫圖。
• 在modelcheck.py中進行模型檢查。
• 在vunarrow.py中縮小範圍。
• 在variants.py中產生變體。
• 迭代gui.py中術語的參數。
• 從buildTerm.py中的符號建立術語。
• 檢查maudedoc.py中的模組。
• 載入檔案並在loading.py中輸入原始文字。
• metalevel.py中的元級別操作。
• hooks.py中的自訂特殊運算子。

此外，文章Maude 作為一個庫：一個高效的通用程式介面提供了有關該程式庫的教程，以及其設計和實現的描述。