Aide à la preuve et à la validation en programmation par règles
Résumé
Nous avons complété une boîte à outils pour la preuve et la vérification de programmes par règles. Nous avons étudié et comparé les différents outils déjà disponibles dans l'environnement, notamment des outils de preuve de terminaison, pour proposer une stratégie optimisée d'utilisation et de coopération de ces outils. Nous avons notamment validé un mécanisme de filtrage d'un programme par l'ordre de plongement, qui permet de faciliter l'utilisation d'ordres plus puissants pour assurer la terminaison d'un programme.