Nous avons 2 langues qui sont (officieusement) sémantiquement équivalentes mais syntaxiquement différentes. L'un est xml et l'autre est basé sur un script. Comment puis-je prouver formellement que les deux langues sont en fait équivalentes? L'approche par script est simplement un moyen pratique d'écrire un même programme qui serait fastidieux à écrire en XML.Équivalence formelle entre les langages de programmation
Merci Ketan
Ecrire un programme qui prend en entrée un programme dans une langue, et donne à sa sortie du programme équivalent dans l'autre langue.
Ensuite, prouver que le programme que vous venez d'écrire est correct pour toutes les entrées possibles.
Une bonne façon de le faire est par une sorte d'induction. Les programmes ont généralement une structure arborescente pour eux; Si vous pouvez prouver que la traduction est correcte pour chaque feuille possible, et vous pouvez prouver qu'elle est correcte pour chaque combinaison possible de deux arbres corrects, alors par induction, vous avez prouvé le tout.
S'il s'agit de langages de programmation généraux, inscrivez un simulateur de machine de Turing dans chacun d'eux. Si ce n'est pas le cas, vous avez plus de problèmes. Êtes-vous sûr que les langues sont équivalentes? Est-ce une sorte d'exploration, ou essayez-vous simplement de prouver ce dont vous êtes déjà sûr?
En général, il n'est pas possible de prouver l'équivalence entre les langues. Si elles ont été écrites indépendamment, votre meilleur pari pourrait être de prouver que le langage basé sur les scripts fait tout ce que vous avez besoin de faire, plutôt que d'essayer de prouver son équivalence à celui basé sur XML.
La première chose que vous devez définir est ce que vous entendez par « équivalent »
Si vous voulez dire « ce que vous pouvez faire avec un, vous pouvez le faire avec l'autre », puis une approche serait de prouver que les deux les langues sont Turing complete Si vous pouvez le faire, alors vous aurez montré que les deux langues peuvent effectuer les mêmes types de calculs (et tout autre langage ou dispositif complet de Turing)
Si vous voulez dire 'ils ont la même structure' juste différentes manières de spécifier les éléments 'alors vous devrez faire abstraction des langues pour montrer qu'elles partagent en effet la même structure. Backus Naur Form est une façon de le faire. Si deux langages ont la même structure dans BNF avec juste les différents terminaux, ils ne sont en réalité que deux représentations différentes de la même syntaxe abstraite.
Il y a évidemment d'autres significations possibles de 'équivalent' et donc d'autres choses que vous pourriez faire.
Vous devez également définir ce que vous entendez par «prouver» - voulez-vous dire une preuve mathématique rigoureuse ou «convaincre mes collègues que le langage de script est assez bon»? Si vous voulez dire le premier, ça va être dur. Si vous voulez dire la seconde, vous pouvez définir une spécification de ce que ces langages doivent être capables de faire et démontrer la preuve de concepts dans chaque langue pour montrer qu'ils peuvent répondre à la spécification.
Vous pouvez prendre un peu d'inspiration ici: http://compcert.inria.fr/doc/index.html
Vous aurez besoin d'aller dans l'autre sens aussi, pour montrer l'équivalence. –