maude bindings

Sprachbindungen für Maude

Sprachbindungen für die Maude-Spezifikationssprache mit SWIG. Sie verwenden eine modifizierte Version von Maude, die um einen Modellprüfer für strategiegesteuerte Systeme erweitert wurde und auf den auch über die Bindungen zugegriffen werden kann.

Das Python-Paket ist bei PyPI verfügbar. Nach der Installation mit pip install maude kann es direkt verwendet werden, da Maude in das Paket eingebettet ist:

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

Bindungen für andere von SWIG unterstützte Sprachen können aus diesem Repository erstellt werden, sie wurden jedoch nicht speziell unterstützt und getestet. Für einige davon finden Sie hier spezifische Anleitungen.

Gebäude

Dieses Repository enthält die erweiterte Version von Maude als Submodul, das zuerst mit git submodule update --init oder einem entsprechenden Git-Befehl geklont werden muss. Um das Python-Paket zu erstellen, wird scikit-build-core über einen der Standardbefehle verwendet:

 python -m build  # or
pip wheel .

Dadurch wird Maude im subprojects erstellt, wofür das Meson-Build-System Ninja und verschiedene externe Bibliotheken und Tools erforderlich sind, wie im Repository beschrieben. Alternativ können kompilierte Versionen von Maude als Bibliothek aus dem Veröffentlichungsbereich heruntergeladen und an den erwarteten Speicherorten abgelegt werden:

• subprojects/maudesmc/installdir/lib für die Bibliotheken und
• subprojects/maudesmc/build für die Headerdatei config.h .

In diesem Fall oder wenn Maude direkt aus seinem Unterverzeichnis erstellt wird, sollte CMAKE_ARGS="-DBUILD_LIBMAUDE=OFF" vor dem vorherigen Befehl hinzugefügt werden.

Bindungen für andere Sprachen können auch direkt mit CMake erstellt werden, wobei srcdir das Verzeichnis ist, in dem das Repository geklont wurde, und language eine der von SWIG unterstützten Sprachen ist:

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

Für einige Sprachziele wird dies ausreichen, für andere sind jedoch zusätzliche Schritte zu erwarten.

Dokumentation

Hier ist eine Dokumentation zum Python-Paket verfügbar, die weitgehend auf andere Zielsprachen übertragen werden kann. Es ist auch eine von Javadoc generierte Dokumentation verfügbar. Darüber hinaus können die Beispiele im Repository als Referenz für verschiedene Themen verwendet werden:

• Laden von Dateien, Parsen von Begriffen, Reduzieren, Umschreiben, Umschreiben mit Strategien und Suchen in test.py
• Matching in match.py ​​.
• Regeln selektiv in apply.py anwenden.
• Vereinheitlichung in unify.py .
• Bearbeiten des Umschreibediagramms in graph.py .
• Modellüberprüfung in modelcheck.py .
• Einengung in vunarrow.py .
• Variantengenerierung in variants.py .
• Durchlaufen der Argumente eines Begriffs in gui.py .
• Begriffe aus Symbolen in buildTerm.py erstellen.
• Module in maudedoc.py prüfen.
• Laden Sie Dateien und geben Sie Rohtext in loading.py ein.
• Metalevel-Manipulationen in metalevel.py .
• Benutzerdefinierte Spezialoperatoren in hooks.py .

Darüber hinaus finden Sie im Artikel Maude als Bibliothek: eine effiziente Allzweck-Programmierschnittstelle ein Tutorial zur Bibliothek sowie eine Beschreibung ihres Designs und ihrer Implementierung.