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 作为一个库：一个高效的通用编程接口提供了有关该库的教程，以及其设计和实现的描述。