maude bindings

Liaisons linguistiques pour Maude

Liaisons de langage pour le langage de spécification Maude utilisant SWIG. Ils utilisent une version modifiée de Maude étendue avec un vérificateur de modèles pour les systèmes contrôlés par des stratégies, qui est également accessible via les liaisons.

Le package Python est disponible sur PyPI. Après l'avoir installé à l'aide pip install maude , il peut être directement utilisé puisque Maude est intégré dans le package :

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

Des liaisons pour d'autres langages pris en charge par SWIG peuvent être créées à partir de ce référentiel, mais elles n'ont pas bénéficié d'un support ni de tests spécifiques. Des instructions spécifiques pour certains d’entre eux sont disponibles ici.

Bâtiment

Ce référentiel inclut la version étendue de Maude en tant que sous-module, qui doit d'abord être cloné avec git submodule update --init ou une commande Git équivalente. Pour créer le package Python, scikit-build-core est utilisé via l'une des commandes standard :

 python -m build  # or
pip wheel .

Cela entraînera la construction de Maude dans le répertoire subprojects , pour lequel le système de construction Meson, Ninja et diverses bibliothèques et outils externes sont requis, comme décrit dans son référentiel. Alternativement, les versions compilées de Maude en tant que bibliothèque peuvent être téléchargées à partir de sa section des versions et placées à leurs emplacements prévus :

• subprojects/maudesmc/installdir/lib pour les bibliothèques, et
• subprojects/maudesmc/build pour le fichier d'en-tête config.h .

Dans ce cas ou lors de la construction de Maude directement à partir de son sous-répertoire, CMAKE_ARGS="-DBUILD_LIBMAUDE=OFF" doit être ajouté avant la commande précédente.

Les liaisons pour d'autres langages peuvent également être créées directement à l'aide de CMake, où srcdir est le répertoire dans lequel le référentiel a été cloné et où language est l'un des langages pris en charge par SWIG :

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

Pour certaines cibles linguistiques, cela sera suffisant, mais des étapes supplémentaires pourraient être attendues pour d’autres.

Documentation

La documentation du package Python est disponible ici, qui peut être largement extrapolée à d'autres langages cibles. La documentation générée par Javadoc est également disponible. En plus de ceux-ci, les exemples du référentiel peuvent être utilisés comme référence pour divers sujets :

• Chargement de fichiers, analyse des termes, réduction, réécriture, réécriture avec des stratégies et recherche dans test.py .
• Correspondance dans match.py ​​.
• Application sélective des règles dans apply.py .
• Unification dans unify.py .
• Manipulation du graphique de réécriture dans graph.py .
• Vérification du modèle dans modelcheck.py .
• Rétrécissement dans vunarrow.py .
• Génération de variantes dans variants.py .
• Itérer sur les arguments d'un terme dans gui.py .
• Création de termes à partir de symboles dans buildTerm.py .
• Inspection des modules dans maudedoc.py .
• Chargement de fichiers et saisie du texte brut dans loading.py .
• Manipulations de niveau métal dans metalevel.py .
• Opérateurs spéciaux personnalisés dans hooks.py .

D'ailleurs, un tutoriel sur la bibliothèque est disponible dans l'article Maude comme bibliothèque : une interface de programmation polyvalente efficace , ainsi qu'une description de sa conception et de sa mise en œuvre.