Un enjeu fondamental de l'informatique est la réalisation de logiciels corrects. Établir la correction d'un logiciel nécessite de disposer au préalable d'une spécification, c'est-à-dire d'une description formelle des fonctionnalités attendues du logiciel. La preuve de la conformité du logiciel avec sa spécification est par ailleurs grandement facilitée lorsque le langage de programmation utilisé est suffisamment abstrait. Lorsque l'on choisit d'écrire aussi bien les spécifications que les programmes dans un style déclaratif avec des formules logiques du premier ordre, on obtient un cadre homogène (spécifications algébriques et langages de programmation logique) pour exprimer et traiter le problème de la validation de logiciel.
La spécification d'un logiciel de grande taille est un objet complexe qu'il est nécessaire de savoir décomposer en modules. Certains de nos travaux portent sur l'étude de primitives de structuration des spécifications algébriques et en particulier sur la modularisation. Un premier objectif est de permettre de ramener le problème de la correction du logiciel global à celui de la correction de chacun de ses modules. Un objectif complémentaire est ensuite de développer des techniques permettant le développement indépendant, par un processus de raffinements successifs, de réalisations pour chacun des modules, et de prouver leur correction (cf. 2).
Une méthode pour assurer la correction a priori d'un programme consiste à le dériver de sa spécification. Par exemple, lorsque la spécification est réduite à un ensemble d'équations conditionnelles positives, elle peut être directement considérée comme un programme logique. Dans le cas où la spécification contient des formules plus générales, la dérivation d'un programme nécessite alors un processus de transformation sophistiqué. Le programme ainsi obtenu est souvent inefficace et il convient d'améliorer le contrôle de son exécution. Des méthodes de transformation fondées sur la théorie de la démonstration (extraction de programmes à partir de preuves, cf. 4) sont développées et diverses techniques d'optimisation héritées à la fois de la programmation fonctionnelle (réécriture) et de la programmation en Prolog (multi-directionnalité) sont étudiées (cf. 3).
Une autre méthode pour assurer la correction d'un programme est de démontrer a posteriori que les formules de la spécification sont des conséquences du programme. La mécanisation du raisonnement par récurrence pour les programmes Prolog (``exécution étendue'') constitue un domaine d'investigation prometteur (cf. 4). Par ailleurs, des extensions du concept de correction conduisent à développer une théorie de l'observabilité pour prendre en compte le fait qu'un programme peut présenter certaines différences avec le comportement prescrit par sa spécification, pourvu que ces différences ne soient pas ``observables'' (cf. 2).
Les différents points évoqués ci-dessus sont détaillés dans les sous-sections suivantes.
Une modélisation algébrique adéquate de la modularité nécessite des outils sémantiques spécifiques comme la théorie des ``classes stratifiées de modèles'' qui repose sur le paradigme suivant : une implémentation (un programme) est considérée comme étant correcte relativement à sa spécification si et seulement si elle détermine une algèbre modèle de la spécification. Cette interprétation, quoique simplificatrice, permet néanmoins de dégager les contraintes hiérarchiques à associer aux primitives de structuration des spécifications modulaires. Dans [403], cette approche de la modularité est étendue à un cadre très général qui permet en particulier d'exprimer des concepts comme la paramétrisation et l'implémentation de façon uniforme, tout en garantissant les propriétés souhaitables de compositionnalité horizontale et verticale. Cependant, en pratique, un programme doit être considéré comme une implémentation correcte d'une spécification dès que les ``différences'' entre l'algèbre qu'il détermine et un modèle de la spécification ne sont pas observables (avec une notion appropriée d'observabilité). Des concepts adéquats d'observabilité, combinés avec la théorie des ``classes stratifiées de modèles'', doivent ainsi permettre d'obtenir une compréhension plus fine de la correction de logiciel.
Dans le cadre des spécifications algébriques, il existe essentiellement deux approches de l'observabilité. La première approche repose sur une notion de validité observationnelle des axiomes de la spécification, définie à l'aide d'une relation d'indistinguabilité entre les valeurs d'une algèbre. La seconde approche utilise une notion d'équivalence observationnelle entre algèbres. Dans un premier temps nous avons réalisé une étude approfondie des différentes notions d'observabilité existantes, en comparant en particulier leur pouvoir d'expression respectif [396].
Plus récemment, et en coopération avec Rolf Hennicker et Martin Wirsing (Ludwig-Maximilians-Universität, Munich), un cadre général permettant de présenter de façon uniforme les approches existantes et de les comparer entre elles a été défini. Nous avons en particulier pu mettre en évidence la dualité existant entre les deux types d'approches, et exhiber une condition nécessaire et suffisante pour qu'elles soient sémantiquement équivalentes, résolvant ainsi un problème ouvert depuis plus de dix ans [402, 398].
Pour que les approches intégrant des concepts d'observabilité deviennent utilisables en pratique, il est nécessaire de développer des méthodes de preuves adaptées à une sémantique observationnelle des spécifications algébriques. Cet aspect a été l'objet d'investigations approfondies (en coopération avec Rolf Hennicker) et nous avons pu dégager des techniques de preuve de propriétés observables. L'intérêt de ces techniques, en dehors de leur généralité, est qu'il est possible de les mettre en oeuvre avec les démonstrateurs existants (comme le Larch Prover, par exemple) [413, 404, 405, 399].
Les résultats ci-dessus ont une portée très générale. Nous cherchons actuellement à les formuler dans le cadre abstrait des institutions (en collaboration avec Andrzej Tarlecki, Académie des Sciences de Varsovie [417]) et nous avons commencé à les appliquer à la preuve de la correction d'implémentations (en coopération avec Rolf Hennicker [406]).
Les aspects de non-déterminisme et de ``multidirectionnalité'' (pas de distinction entre entrées et sorties) constituent des atouts de la programmation logique dont ne bénéficie pas la programmation fonctionnelle. De son côté, la programmation fonctionnelle présente un certain nombre d'avantages sur la programmation logique. Citons en particulier la possibilité de contrôler plus efficacement et de façon plus transparente l'exécution des programmes (évaluation paresseuse, stricte, ...). Il y a donc un grand intérêt à chercher à intégrer programmation logique et programmation fonctionnelle Les solutions étudiées considèrent des langages fonctionnels qui sont étendus pour incorporer la notion de variable logique (par exemple SLOG et K-LEAF) et cherchent à ``compiler'' les programmes écrits dans de tels langages sous forme de programmes Prolog [392].
Le principe de la programmation déclarative facilite le problème de validation du logiciel. Pour vérifier qu'un programme logique satisfait une certaine propriété, il suffit en effet de prouver que la propriété est conséquence des clauses du programme. On s'intéresse ainsi au seul contenu logique des programmes, en s'affranchissant des problèmes liés au contenu algorithmique.
La procédure d'exécution étendue, inventée par Kanamori et son équipe à Mitsubishi, est une extension de l'interpréteur Prolog qui permet de prouver d'intéressantes propriétés de programmes logiques. Cette procédure utilise le mécanisme de résolution de l'interpréteur Prolog, mais incorpore également un principe de récurrence ainsi que divers raffinements [393]. La procédure est ainsi capable de prouver des propriétés beaucoup plus générales que les requêtes posées traditionnellement en Prolog : les propriétés qui sont soumises à l'interpréteur étendu peuvent être considérées comme de véritables spécifications logiques.
Par ailleurs, une procédure de décision pour la théorie des listes d'entiers a été intégrée dans l'interpréteur, reposant sur un mécanisme d'évaluation ascendante [422, 410]. Elle a été récemment appliquée à la spécification et la preuve de propriétés d'automates communicants [421, 415, 400], et comparée avec des méthodes d'évaluation descendante [423].
L'équipe Spécifications algébriques et Programmation logique a été dissoute fin 96 suite au départ de Michel Bidoit et Laurent Fribourg à l'ENS de Cachan.