Traduire des fonctions récursives de VDM à Isabelle/HOL

Cet article parle d'une méthode pour traduire des définitions récursives d'un système appelé VDM vers un autre système connu sous le nom d'Isabelle/HOL. L'objectif est de créer des modèles qui peuvent gérer automatiquement différents types de définitions dans VDM. Cette méthode se concentre sur le fait de s'assurer que les traductions sont claires et qu'elles automatisent autant que possible le processus de preuve.

VDM et Isabelle/HOL ont quelques différences, surtout dans la façon dont ils traitent le concept de terminaison dans les Fonctions Récursives. La terminaison est importante parce qu'elle garantit qu'une fonction ne va pas tourner indéfiniment. L'article va discuter de la façon dont on peut traduire des définitions récursives tout en tenant compte de ces différences.

Avec cette méthode de traduction, on apporte une extension aux outils existants qui aident les utilisateurs à convertir les définitions VDM en Isabelle/HOL. Isabelle permet aux utilisateurs d'écrire des spécifications, des preuves et de la documentation au même endroit. Les détails complets des sources et des preuves impliquées se trouvent dans un dépôt d'outils spécifique.

Les sections suivantes vont fournir des infos de base sur VDM et Isabelle, suivies de discussions sur la traduction des types de base, de la récursion et de la stratégie de traduction globale.

#Contexte

Le traducteur de VDM vers Isabelle/HOL couvre un large éventail de structures trouvées dans VDM. Il peut gérer diverses expressions, motifs, types et spécifications dans VDM. Le but est de s'assurer que la plupart des motifs en VDM peuvent être traduits efficacement, et quand ce n'est pas le cas, il y aura une façon équivalente de les représenter.

Un domaine clé de la traduction est la gestion des fonctions définies récursivement. Dans VDM, les utilisateurs doivent définir une fonction de mesure pour s'assurer que la récursion va se terminer. Cette fonction de mesure génère des obligations de preuve, qui sont des exigences à confirmer que la récursion fonctionne comme prévu.

La stratégie de traduction utilisée ici suit une approche spécifique appelée terminaison par changement de taille (SCT). Cette approche vérifie si une fonction récursive peut être prouvée comme se terminant en fonction des valeurs qu'elle produit. Si chaque computation conduit à une valeur plus petite, on peut s'assurer que la récursion va finalement s'arrêter.

#Types de base VDM dans Isabelle

Dans Isabelle, les nombres naturels sont représentés comme un type de données avec deux parties : le nombre zéro et une fonction successeur qui ajoute un. Isabelle définit aussi des entiers et d'autres types numériques en utilisant ces nombres naturels. Des conversions de type sont disponibles pour aider les utilisateurs à passer d'un type à l'autre, mais il n'y a pas de règles implicites qui élargissent les types automatiquement.

Dans VDM, les types de base comme les nombres naturels et les entiers ont des règles d'élargissement spécifiques qui doivent être prises en compte. Par exemple, si les deux types sont des nombres naturels, le résultat pourrait être un entier. Notre stratégie de traduction traite les nombres naturels de VDM spécifiquement comme un synonyme de type dans Isabelle, ce qui aide à simplifier le processus et à éviter le besoin de coercitions de type compliquées.

Cependant, cela signifie que coder des fonctions récursives en utilisant des nombres naturels peut être plus complexe que prévu, car la représentation dans Isabelle diffère de celle dans VDM.

Même avec ces complexités, la récursion sur des entiers, des ensembles ou des cartes dans VDM se produit toujours car ces types n'ont pas de définition constructive simple dans Isabelle.

#Récursion dans VDM et Isabelle

Chaque définition récursive nécessite un moyen de justifier qu'elle va se terminer. Sinon, la récursion peut mener à une boucle infinie. Dans VDM, cette justification vient de la mesure récursive, qui prend les mêmes entrées que la définition récursive et retourne un nombre naturel qui doit diminuer à chaque appel récursif.

Par exemple, considérons une simple fonction récursive qui calcule la factorielle d'un nombre naturel. La fonction de mesure utilise l'entrée elle-même, et la récursion s'arrête quand cette entrée atteint zéro. Dans ce cas, VDM génère trois obligations de preuve qui doivent être confirmées dans Isabelle.

Isabelle, quant à elle, permet des définitions récursives par la récursion primitive ou des définitions de fonctions générales qui produisent des obligations de preuve. Le défi réside dans le fait de s'assurer que les paramètres correspondent aux motifs définis et que les appels récursifs vont se terminer correctement.

Les définitions de fonctions récursives d'Isabelle peuvent être exprimées en utilisant deux types de syntaxe : une qui essaie de prouver automatiquement la terminaison et une autre qui nécessite que les utilisateurs fournissent manuellement la preuve de la terminaison. Ce dernier est souvent nécessaire dans les cas où la fonction récursive est plus complexe.

La relation de terminaison doit également être bien fondée, ce qui signifie qu'elle doit avoir une structure ordonnée pour garantir que la récursion se terminera. Cette exigence ajoute une autre couche de complexité au processus de traduction.

#Stratégie de traduction de récursion VDM

L'objectif de la stratégie de traduction est de traiter les problèmes liés à la récursion sur des types de base, des ensembles, des séquences et des cartes, y compris la récursion mutuelle. On commence par étiqueter toutes les fonctions récursives dans VDM, même celles sans mesure explicite, pour faciliter la traduction en utilisant les fonctions d'Isabelle.

Si Isabelle échoue à prouver automatiquement la terminaison nécessaire, l'utilisateur peut fournir une annotation qui définit une relation de mesure bien fondée. Cela aide à établir la relation entre les appels récursifs et garantit que la traduction réussira.

Pendant la traduction, l'outil vérifie l'annotation pour s'assurer qu'elle est correctement définie. Ce processus implique de traduire les Annotations en définitions Isabelle pour soutenir la preuve de terminaison.

La stratégie de traduction exige également que les vérifications VDM soient explicitement déclarées comme des prédicats. Par exemple, les ensembles VDM doivent être finis, et leurs invariants de type doivent tenir pour chaque élément.

#Récursion sur les types de base VDM

Pour les types de base comme les nombres naturels, la stratégie de traduction commence par établir une précondition qui exige que le paramètre soit un type valide. Ensuite, on définit la fonction récursive, retournant une valeur indéfinie si la précondition échoue. Les preuves de compatibilité et de complétude des motifs sont ensuite établies selon les méthodes standard d'Isabelle.

La bien-fondée de la récursion peut souvent être établie en utilisant le matériel existant d'Isabelle, rendant le processus plus fluide. On définit aussi de nouveaux lemmas pour aider à la découverte de preuves, ce qui aide à réduire la charge sur l'utilisateur.

#Récursion sur les ensembles VDM

La prochaine étape dans la stratégie de traduction implique la gestion des ensembles VDM. Un exemple courant est une fonction qui somme les éléments d'un ensemble. La fonction vérifie si l'ensemble est vide avant de procéder à la somme, choisissant un élément arbitraire à utiliser dans la récursion.

On définit une précondition pour la fonction qui s'assure que l'ensemble ne contient que des nombres valides et est fini. Comme avec les types de base, on établit la fonction récursive dans Isabelle, vérifiant la précondition avant d'exécuter la somme.

La relation de mesure doit refléter les processus impliqués, et les outils d'Isabelle peuvent être utilisés pour valider la bien-fondée de la relation. La preuve de terminaison est également construite sur les préconditions précédentes et les conditions de filtrage.

#Récursion sur les cartes VDM

La récursion sur les cartes est similaire à la récursion sur les ensembles. Une fonction qui somme les valeurs d'une carte utilise des techniques similaires en vérifiant si la carte est vide et, si ce n'est pas le cas, en choisissant une clé pour sommer la valeur qui lui est associée.

Comme avant, les préconditions s'assurent que le domaine et l'image de la carte satisfont les propriétés nécessaires. Le processus de traduction vérifie les conditions de bien-fondement et construit la relation de mesure appropriée pour soutenir la preuve de terminaison.

#Récursion impliquant des mesures complexes

On peut aussi appliquer la même approche de traduction à des définitions récursives plus complexes. Cependant, ces définitions nécessitent souvent que les utilisateurs définissent des annotations plus détaillées et des lemmes supplémentaires pour soutenir le processus de preuve.

Par exemple, considérons la fonction d'Ackermann, connue pour sa récursion complexe. La fonction exige que les deux paramètres soient traités d'une certaine manière, ce qui implique des mesures supplémentaires qui doivent être définies dans VDM. Les utilisateurs doivent fournir des annotations pour aider Isabelle à inférer correctement les relations entre les appels récursifs.

Les mesures utilisées dans la version VDM diffèrent de celles généralement vues dans Isabelle, donc il est essentiel d'établir une connexion claire entre les deux pour que la traduction fonctionne.

#Exemples plus difficiles

Certains exemples sont plus difficiles et nécessitent une configuration plus élaborée pour la preuve. Par exemple, la fonction de permutation montre comment elle peut permuter entre des paramètres décroissants, et la fonction de Takeuchi illustre la récursion interne.

Ces exemples complexes révèlent souvent comment les systèmes de preuve peuvent différer dans leurs exigences. Les utilisateurs doivent fournir des mesures spécifiques et effectuer souvent des interventions manuelles pour aider Isabelle à générer les preuves nécessaires.

#Récursion mutuelle

Enfin, la traduction prend également en compte la récursion mutuelle, où VDM permet des définitions qui s'appellent mutuellement. On peut utiliser des algorithmes du vérificateur de types de VDM pour identifier ces relations et déduire les mesures nécessaires.

Si le graphe de récursion ne peut pas être découvert automatiquement, les utilisateurs doivent annoter l'une des définitions récursives mutuelles pour indiquer les noms des fonctions attendues impliquées.

Essentiellement, ces interactions exigent que toutes les fonctions liées soient définies ensemble pour garantir un bon lien dans la configuration de la preuve.

#Conclusion

Cet article a décrit une méthode pour traduire des fonctions récursives de VDM vers Isabelle/HOL, en se concentrant sur les types de base, les ensembles, les cartes et la récursion mutuelle. Les stratégies discutées permettent une large variété de définitions récursives, y compris des exemples complexes qui nécessitent des mesures supplémentaires et une interaction de l'utilisateur.

Alors qu'on continue à affiner cette stratégie de traduction, elle va devenir un outil précieux pour les utilisateurs ayant besoin de convertir leurs définitions VDM en Isabelle/HOL tout en s'assurant de la correction et de la terminaison de leurs fonctions récursives. Les travaux futurs impliquent de mettre en œuvre davantage ces stratégies dans des outils existants pour améliorer l'utilisabilité et l'automatisation pour les utilisateurs.