Génération automatique de code O'Caml à partir de spécifications CASL

Dans cet article nous présentons un générateur de code O'CAML à partir de spécifications formelles CASL. Il produit du code pour des spécifications aux formes variées, comprenant des opérations totales, des opérations partielles et des prédicats définis par des axiomes équationnels. Nous assurons la correction du code produit par les propriétés, de terminaison, confluence et complétude, du système de réécriture équivalent aux axiomes que nous obtenons en orientant ceux-ci de gauche à droite. Le générateur vérifie automatiquement ces propriétés (et donc la correction) lorsque la spécification traitée respecte des contraintes syntaxiques suffisantes. Dans le cas contraire le générateur produit des obligations de preuves, qui devront être vérifiées par l'utilisateur pour garantir la correction du code généré. Nous obtenons un code lisibile en préservant au maximum les choix syntaxiques de la spécification de départ : nom des identificateurs, ordre des définitions, commentaires, etc.