Traduciendo funciones recursivas de VDM a Isabelle/HOL

Este artículo habla sobre un método para traducir definiciones recursivas de un sistema llamado VDM a otro sistema conocido como Isabelle/HOL. El objetivo es crear plantillas que puedan manejar automáticamente muchos tipos diferentes de definiciones en VDM. Este método se enfoca en asegurar que las traducciones sean claras y que automaticen lo máximo posible el proceso de prueba.

VDM e Isabelle/HOL tienen algunas diferencias, especialmente en cómo manejan el concepto de Terminación en Funciones Recursivas. La terminación es importante porque asegura que una función no se ejecute para siempre sin detenerse. El artículo discutirá cómo podemos traducir definiciones recursivas teniendo en cuenta estas diferencias.

Usando este método de traducción, ofrecemos una extensión a herramientas existentes que ayudan a los usuarios a convertir definiciones de VDM a Isabelle/HOL. Isabelle permite a los usuarios escribir especificaciones, pruebas y documentación todo en un solo lugar. Los detalles completos de las fuentes y pruebas involucradas se pueden encontrar en un repositorio específico de herramientas.

Las próximas secciones ofrecerán información de fondo sobre VDM e Isabelle, seguidas de discusiones sobre la traducción de tipos básicos, recursión y la estrategia general de traducción.

#Antecedentes

El traductor de VDM a Isabelle/HOL cubre una amplia gama de estructuras encontradas en VDM. Puede manejar varias expresiones, patrones, tipos y especificaciones en VDM. El objetivo es garantizar que la mayoría de los patrones en VDM puedan ser traducidos de manera efectiva y, cuando no, habrá una forma equivalente de representarlos.

Un área clave en este tipo de traducción es el manejo de funciones definidas recursivamente. En VDM, los usuarios deben definir una función de medida para asegurarse de que la recursión terminará. Esta función de medida genera obligaciones de prueba, que son requisitos para confirmar que la recursión funciona como se espera.

La estrategia de traducción utilizada aquí sigue un enfoque específico llamado terminación por cambio de tamaño (SCT). Este enfoque verifica si se puede probar que una función recursiva termina en función de los valores que produce. Si cada cálculo conduce a un valor más pequeño, se puede garantizar que la recursión eventualmente se detendrá.

#Tipos Básicos de VDM en Isabelle

En Isabelle, los números naturales se representan como un tipo de dato con dos partes: el número cero y una función sucesora que suma uno. Isabelle también define enteros y otros tipos numéricos usando estos números naturales. Las conversiones de tipo están disponibles para ayudar a los usuarios a pasar entre tipos, pero no hay reglas implícitas que amplíen tipos automáticamente.

En VDM, tipos básicos como números naturales y enteros tienen reglas específicas de ampliación que deben ser consideradas. Por ejemplo, si ambos tipos son números naturales, el resultado podría ser un entero. Nuestra estrategia de traducción trata a los números naturales de VDM específicamente como un sinónimo de tipo en Isabelle, lo que ayuda a simplificar el proceso y evita la necesidad de coerciones de tipo complicadas.

Sin embargo, esto significa que codificar funciones recursivas usando números naturales puede ser más complejo de lo esperado, ya que la representación en Isabelle difiere de la de VDM.

Aún con estas complejidades, la recursión sobre enteros, conjuntos o mapas en VDM sigue ocurriendo porque estos tipos no tienen una definición constructiva sencilla en Isabelle.

#Recursión en VDM e Isabelle

Cada definición recursiva requiere una forma de justificar que terminará. De lo contrario, la recursión puede llevar a un bucle infinito. En VDM, esta justificación proviene de la medida recursiva, que toma las mismas entradas que la definición recursiva y devuelve un número natural que debe disminuir con cada llamada recursiva.

Por ejemplo, considera una función recursiva simple que calcula el factorial de un número natural. La función de medida usa la entrada misma, y la recursión se detiene cuando esta entrada llega a cero. En este caso, VDM genera tres obligaciones de prueba que deben ser confirmadas en Isabelle.

Isabelle, por otro lado, permite definiciones recursivas a través de recursión primitiva o definiciones de funciones generales que producen obligaciones de prueba. El desafío radica en asegurarse de que los parámetros coincidan con los patrones definidos y que las llamadas recursivas terminen correctamente.

Las definiciones de funciones recursivas de Isabelle pueden expresarse usando dos tipos de sintaxis: una que intenta probar automáticamente la terminación y otra que requiere que los usuarios proporcionen manualmente la prueba de terminación. Esta última a menudo es necesaria en casos donde la función recursiva es más compleja.

La relación de terminación también debe ser bien fundada, lo que significa que debe tener una estructura ordenada para garantizar que la recursión terminará. Este requisito agrega otra capa de complejidad al proceso de traducción.

#Estrategia de Traducción de Recursión en VDM

El objetivo de la estrategia de traducción es abordar los problemas relacionados con la recursión sobre tipos básicos, conjuntos, secuencias y mapas, incluida la recursión mutua. Comenzamos etiquetando todas las funciones recursivas en VDM, incluso aquellas sin una medida explícita, para facilitar la traducción usando las funciones de Isabelle.

Si Isabelle no logra probar automáticamente la terminación necesaria, el usuario puede proporcionar una Anotación que defina una relación de medida bien fundada. Esto ayuda a establecer la relación entre las llamadas recursivas y asegura que la traducción tendrá éxito.

Durante la traducción, la herramienta verifica la anotación para asegurarse de que esté correctamente definida. Este proceso implica traducir las anotaciones en definiciones de Isabelle para apoyar la prueba de terminación.

La estrategia de traducción también requiere que las verificaciones de VDM se expresen explícitamente como predicados. Por ejemplo, los conjuntos de VDM deben ser finitos, y sus invariantes de tipo deben sostenerse para cada elemento.

#Recursión sobre Tipos Básicos de VDM

Para tipos básicos como números naturales, la estrategia de traducción primero establece una precondición que insiste en que el parámetro es un tipo válido. A continuación, definimos la función recursiva, devolviendo un valor indefinido si la precondición falla. Las pruebas de compatibilidad y completitud de los patrones se establecen siguiendo métodos estándar de Isabelle.

La bien fundación de la recursión a menudo puede establecerse utilizando la maquinaria existente de Isabelle, lo que facilita el proceso. También definimos nuevos lemas para ayudar con la descubrimiento de pruebas, lo que ayuda a reducir la carga sobre el usuario.

#Recursión sobre Conjuntos de VDM

El siguiente paso en la estrategia de traducción implica manejar conjuntos de VDM. Un ejemplo común es una función que suma los elementos de un conjunto. La función verifica si el conjunto está vacío antes de proceder con la suma, eligiendo un elemento arbitrario para usar en la recursión.

Definimos una precondición para la función que asegura que el conjunto solo contenga números válidos y sea finito. Al igual que con los tipos básicos, establecemos la función recursiva en Isabelle, verificando la precondición antes de ejecutar la suma.

La relación de medida debe reflejar los procesos involucrados, y se pueden usar las herramientas de Isabelle para validar la bien fundación de la relación. La prueba de terminación también se construye sobre las precondiciones previas y condiciones de filtrado.

#Recursión sobre Mapas de VDM

La recursión sobre mapas es similar a la recursión sobre conjuntos. Una función que suma los valores de un mapa utiliza técnicas similares verificando si el mapa está vacío y, si no, eligiendo una clave para sumar el valor asociado.

Como antes, las precondiciones aseguran que tanto el dominio como el rango del mapa satisfacen las propiedades necesarias. El proceso de traducción verifica las condiciones principales de bien fundación y construye la relación de medida apropiada para respaldar la prueba de terminación.

#Recursión que Involucra Medidas Complejas

También podemos aplicar el mismo enfoque de traducción a definiciones recursivas más complejas. Sin embargo, estas definiciones a menudo requieren que los usuarios definan anotaciones más detalladas y lemas adicionales para respaldar el proceso de prueba.

Por ejemplo, considera la conocida función de Ackermann, que se caracteriza por su compleja recursión. La función requiere que se procesen ambos parámetros de cierta manera, lo que implica medidas adicionales que deben definirse en VDM. Los usuarios deben proporcionar anotaciones para ayudar a Isabelle a inferir correctamente las relaciones entre las llamadas recursivas.

Las medidas utilizadas en la versión de VDM difieren de las que típicamente se ven en Isabelle, por lo que es esencial establecer una conexión clara entre las dos para que la traducción funcione.

#Ejemplos Más Difíciles

Algunos ejemplos son más desafiantes y requieren una configuración más elaborada para la prueba. Por ejemplo, la función de permutación muestra cómo puede permutar entre parámetros decrecientes, y la función Takeuchi muestra recursión interna.

Estos ejemplos complejos a menudo revelan cómo los sistemas de prueba pueden diferir en sus requisitos. Los usuarios deben proporcionar medidas específicas y, a menudo, hacer intervenciones manuales para ayudar a Isabelle a generar las pruebas necesarias.

#Recursión Mutua

Finalmente, la traducción también toma en cuenta la recursión mutua, donde VDM permite definiciones que se llaman entre sí. Podemos usar algoritmos del verificador de tipos de VDM para identificar estas relaciones y deducir las medidas necesarias.

Si el grafo de recursión no puede descubrirse automáticamente, los usuarios deben anotar una de las definiciones recursivas mutuas para indicar los nombres de las funciones esperadas involucradas.

Esencialmente, estas interacciones requieren que todas las funciones relacionadas se definan juntas para asegurar un enlace adecuado en la configuración de la prueba.

#Conclusión

Este artículo ha esbozado un método para traducir funciones recursivas de VDM a Isabelle/HOL, enfocándose en tipos básicos, conjuntos, mapas y recursión mutua. Las estrategias discutidas permiten una amplia variedad de definiciones recursivas, incluyendo ejemplos complejos que requieren medidas adicionales e interacción del usuario.

A medida que continuemos refinando esta estrategia de traducción, se convertirá en una herramienta valiosa para los usuarios que necesiten convertir sus definiciones de VDM a Isabelle/HOL mientras aseguran la corrección y terminación de sus funciones recursivas. El trabajo futuro implica implementar aún más estas estrategias en herramientas existentes para mejorar la usabilidad y automatización para los usuarios.