maude bindings

Enlaces de idiomas para Maude

Enlaces de idioma para el lenguaje de especificación Maude usando SWIG. Hacen uso de una versión modificada de Maude ampliada con un verificador de modelos para sistemas controlados por estrategias, al que también se puede acceder a través de enlaces.

El paquete Python está disponible en PyPI. Después de instalarlo usando pip install maude , se puede usar directamente ya que Maude está integrado en el paquete:

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

Desde este repositorio se pueden crear enlaces para otros lenguajes admitidos por SWIG, pero no se les ha brindado soporte ni pruebas específicas. Las instrucciones específicas para algunos de ellos están disponibles aquí.

Edificio

Este repositorio incluye la versión extendida de Maude como un submódulo, que debe clonarse primero con git submodule update --init o un comando Git equivalente. Para construir el paquete Python, se usa scikit-build-core a través de cualquiera de los comandos estándar:

 python -m build  # or
pip wheel .

Esto hará que Maude se construya en el directorio subprojects , para lo cual se requiere el sistema de compilación Meson, Ninja y varias bibliotecas y herramientas externas, como se describe en su repositorio. Alternativamente, las versiones compiladas de Maude como biblioteca se pueden descargar desde su sección de lanzamientos y colocarlas en las ubicaciones esperadas:

• subprojects/maudesmc/installdir/lib para las bibliotecas, y
• subprojects/maudesmc/build para el archivo de encabezado config.h .

En este caso o al compilar Maude directamente desde su subdirectorio, se debe agregar CMAKE_ARGS="-DBUILD_LIBMAUDE=OFF" antes del comando anterior.

Los enlaces para otros idiomas también se pueden crear usando CMake directamente, donde srcdir es el directorio donde se clonó el repositorio y language es uno de los idiomas admitidos por SWIG:

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

Para algunos objetivos lingüísticos esto será suficiente, pero en otros se podrían esperar pasos adicionales.

Documentación

La documentación para el paquete Python está disponible aquí, que se puede extrapolar en gran medida a otros lenguajes de destino. La documentación generada por Javadoc también está disponible. Además de estos, los ejemplos del repositorio se pueden utilizar como referencia para varios temas:

• Cargar archivos, analizar términos, reducir, reescribir, reescribir con estrategias y buscar en test.py
• Coincidencia en match.py .
• Aplicar reglas de forma selectiva en apply.py .
• Unificación en unify.py .
• Manipular el gráfico de reescritura en graph.py .
• Comprobación de modelos en modelcheck.py .
• Estrechamiento en vunarrow.py .
• Generación de variantes en variants.py .
• Iterando sobre los argumentos de un término en gui.py
• Construyendo términos a partir de símbolos en buildTerm.py .
• Inspeccionando módulos en maudedoc.py .
• Cargando archivos e ingresando texto sin formato en loading.py .
• Manipulaciones de metalevel en metalevel.py .
• Operadores especiales personalizados en hooks.py .

Además, hay disponible un tutorial sobre la biblioteca en el artículo Maude como biblioteca: una interfaz de programación eficiente para todo propósito , junto con una descripción de su diseño e implementación.