Abstract FR:

Dans le processus de specification d'un systeme se pose toujours le probleme du choix du langage dans lequel cette specification doit etre formulee. Nous presentons, la methode de specification qui a ete proposee par p. Deransart et g. Ferrand et qui est basee sur les programmes normaux quelconques, ensuite nous nous limitons aux cas stratifies. Un programme ecrit dans ce langage est considere comme une specification. A chaque paquet de clauses d'une specification est associee une assertion semi-formelle. Les assertions traduisent partiellement la semantique attendue de la specification. La methodologie sous-jacente pour l'elaboration et la mise en uvre des preuves de correction partielle et de completude est presentee. Cette methode a ete utilisee pour specifier prolog standard. Nous presentons, dans une seconde etape, un algorithme de calcul de la stratification minimale d'un programme stratifie. Nous discutons egalement la derivation d'une specification executable a partir d'une specification formelle ecrite dans le langage evoque ci-dessus. Nous illustrons ceci par l'exemple de prolog standard. Enfin, nous introduisons une utilisation originale du typage pour un diagnostic pertinent des erreurs dans des programmes en logique. Plus precisement, nous proposons d'ajouter au programme des declarations de types avec quelques cas d'erreurs ainsi que des declarations de profils. Nous generons ensuite automatiquement les clauses de cas d'erreurs relatifs a chaque predicat. Ce systeme peut etre utilise dans la mise au point de programmes en logique. Une application directe du systeme pour la validation des specifications des cas d'erreurs des predicats predefinis de prolog standard est presentee