ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 27/8 - 2008  - pp.1033-1064  - doi:10.3166/tsi.27.1033-1064
TITRE
Un système vérifiant des propriétés opérationnelles de programmes logiques

RÉSUMÉ
Un analyseur statique de programmes logiques est présenté. Le système est construit selon un cadre unifié d'interprétation abstraite, permettant l'intégration de plusieurs domaines et analyses servant à la vérification et à l'optimisation automatiques de programmes logiques. L'analyseur vérifie de nombreuses propriétés désirables de programmes logiques, en tenant compte de la recherche en profondeur d'abord, et des autres caractéristiques spécifiques de Prolog. Les propriétés opérationnelles vérifiées concernent les types, les modes, la linéarité, le partage de variables entre les termes, la preuve de terminaison, la non nécessité du test d'occurrence lors de l'unification, le succès ou l'échec certain, le déterminisme des procédures logiques, les relations linéaires entre les tailles des termes en entrée et en sortie, ainsi que le nombre de solutions pour une requête donnée. L'article met en évidence l'interopérabilité entre les différents domaines qui coopèrent entre eux. Cette contribution mutuelle entre les domaines est nécessaire pour la vérification des propriétés sus-mentionnées.


ABSTRACT
An implemented static analyser of logic programs is presented. The system is based on a unified abstract interpretation framework, which allows the integration of several analyses devoted to verification and optimisation. The analyser is able to verify many desirable properties of logic programs executed with the search-rule and other specific features of Prolog. Such operational properties include verifying type, mode, sharing, and linearity of terms, proving termination, occur-check freeness, sure success or failure, determinacy of logic procedures, as well as linear relations between the size of input/output terms and the number of solutions to a call. It is emphasized how each analysis contributes to each other.


AUTEUR(S)
François GOBERT, Baudouin LE CHARLIER

MOTS-CLÉS
détection statique d'erreurs, interprétation abstraite, vérification automatique, Prolog.

KEYWORDS
abstract debugging, abstract interpretation, automated verification, Prolog.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (480 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier