Ce mémoire décrit le fonctionnement d'un analyseur dédié à la vérification automatique de programmes Prolog, et se basant sur la théorie de l'interprétation abstraite pour atteindre cet objectif. Il s'agira d'interpréter de manière abstraite un programme Prolog et d'en extraire les propriétés sémantiques utiles pour vérifier sa correction. L'interprétation abstraite se fera à l'aide d'un algorithme générique simulant le fonctionnement de Prolog, et les propriétés concernées sont les modes, les types, le formes, les tailles, les partages de variable et de valeur, et les relations existantes entre les termes d'une substitution. Seront également capturées les propriétés des séquences de substitutions retournées par Prolog. Cette interprétation s'inscrit dans le cadre d'une méthodologie de développement inspirée de Y. Deville et considère de manière prioritaire les spécifications et contraintes définies par l'utilisateur. La vérification d'un programme consistera en la comparaison des propriétés du programme capturées par l'interprétation avec les spécifications et contraintes définies par l'utilisateur. L'analyseur réalisant cette vérification peut être à la base de multiples applications ayant pour objectif l'optimisation de programmes Prolog.
Vérification automatique de programmes Prolog basée sur l'interprétation abstraite
Pierard, B. (Auteur). 1997
Student thesis: Master types › Master en sciences informatiques