Abstract FR:

La contribution de cette thèse est double: d'une part, il s'agit d'étudier le problème de la validation de propriétés déclaratives de programmes logiques dans un contexte compositionnel, d'autre part de proposer une extension de la programmation logique au parallélisme de données. L'absence de compositionnalité des sémantiques utilisées en programmation logique a engendré des difficultés a concevoir un système de modules qui lui seraient adapté, et donc des méthodes de validation modulaires. Nous nous proposons de répondre à cette question en définissant d'une part des extensions compositionnelles pour deux sémantiques classiques : la sémantique bien-fondée et la sémantique de Fitting, et d'autre part des méthodes de validation modulaires concernant des propriétés déclaratives pour ces deux sémantiques. L'assurance de la correction d'un programme est obtenue simplement à partir de la correction des modules le composant. L'application de ce formalisme est faite dans le cadre du système de modules de Godel et dans celui de la programmation logique inductive. Le parallélisme de données consiste à appliquer la même opération simultanément sur des données différentes. Nous présentons une proposition de langage de programmation logique, appelée DP-LOG intégrant les concepts du modèle de programmation à parallélisme de données. Il permet la manipulation globale de vecteurs et dispose d'une primitive de communication générale permettant la délocalisation d'une partie de la preuve. Nous lui donnons une sémantique déclarative et une sémantique opérationnelle. Une application possible est le prototypage de programmes massivement parallèles