Cette thèse se place dans le cadre du développement d'un environnement de travail pour la production de logiciels et de leurs démonstrations mathématiques par des méthodes formelles, qui s'appuie en particulier sur des outils améliorant les moyens d'interaction entre l'ordinateur et l'utilisateur.
Dans ce cadre, nous nous appuyons sur les recherches effectuées ces dernières années dans l'équipe CROAP, puis l'équipe LEMME, sur l'outil d'affichage bi-dimensionnel, incrémental, et multi-thread Figue et son extension Aïoli pour la manipulation d'objets arborescents.
D'une part Figue et Aïoli permettent de
présenter les formules mathématiques (indices, exposants, racines,
intégrales, matrices etc...) de façon conviviale et proche des
habitudes des mathématiciens. Ils permettent aussi des interactions variées à
la souris comme la sélection de sous-expressions.
D'autre part la modularité des spécifications d'affichage (PPML) permet à
l'utilisateur d'étendre ses notations selon ses besoins, à l'aide de règles
de grammaire. Cette possibilité d'extension est encore aujourd'hui lourde à
gérer. Cette thèse devrait permettre d'offrir à l'utilisateur une panoplie
d'outils nouveaux, en particulier des outils de debogage de l'affichage
(déterminer quelle règle a affiché une expression donnée par exemple) et des
outils d'aide à la création de nouvelles règles et de nouvelles notations.
En complément d'un affichage riche nous voulons nous appuyer sur les travaux de Stéphane Lavirotte (thèse dirigée par Loïc Pottier) qui portent sur la reconnaissance de formules mathématiques, imprimées ou manuscrites (étant donnés les caractères de la formule, leurs positions et leurs tailles, il s'agit de reconstruire la structure d'une formule pour obtenir sa représentation arborescente). La reconnaissance de formules mathématiques, combinée avec un affichage actif (formules et sous-formules selectionnables) serait un moyen riche d'interaction entre le système et l'utilisateur dans le cadre de developpemenents mathématiques et de preuves.
Une voie de recherche intéressante et originale est ouverte par le problème que poserait la coexistence cohérente de règles de grammaire d'affichage et de saisie. Il s'agirait d'unifier, au moins en partie, les deux formalismes (PPML et réécriture de graphes) de manière à permettre un maintien automatique de leur cohérence en cas de modification par l'utilisateur de l'une ou l'autre des grammaires (affichage ou saisie).
De façon plus prospective, nous voulons compléter cette investigation pour mieux comprendre comment ces différents outils peuvent interagir avec les outils de visualisation existants ou en cours de développement pour le Web.
Intégrer nos outils d'interface sur le Web nous permettra de bénéficier des développements effectués dans les navigateurs et d'atteindre une population plus large d'utilisateurs potentiels d'outils mathématiques sur ordinateur. Nous comptons explorer deux approches: d'une part les outils que nous développons sont écrits en Java, ce qui permet une intégration aisée dans les navigateurs Web les plus répandus. Il est alors possible d'envisager que les utilisateurs téléchargent nos modules comme de simples applets; d'autre part, les navigateurs Web sont déjà construits pour manipuler des données structurées (XML), et, dans une moindre mesure, des objets mathématiques (MathML). Il devrait être possible d'utiliser directement ces primitives de manipulation pour gérer l'ensemble des données utilisées par notre environnement, et lui permettre alors une utilisation et une diffusion faciles via le Web.