Afin de formaliser les possibilités de réutilisation et de transformation du langage Eiffel//, nous menons depuis quelque temps une action de formalisation de la sémantique d'Eiffel//.
Nous avons tout d'abord défini une sémantique opérationnelle du langage Eiffel [1], ceci dans le but d'obtenir une description formelle et opérationnelle d'Eiffel//. Cette deuxième phase est en cours; elle est menée conjointement avec le projet CROAP de l'INRIA Sophia Antipolis et donne lieu à une collaboration avec l'IRIT de Toulouse, dans un projet du GDR/PRC Programmation, avec USC (Los Angeles) et l'université d'Adelaïde (Australie).
Par ailleurs, nous débutons actuellement une formalisation du langage
Eiffel// fondé sur le -calcul. Ce type de sémantique, complémentaire
des techniques opérationnelles décrites ci-dessus, devrait nous
permettre de prouver des équivalences entre systèmes Eiffel//, et de
valider ainsi les transformations automatiques ou semi-automatiques
réalisées pour mener la parallélisation et la réutilisation.
Cette sémantique de type
-calcul est définie en collaboration
avec le projet MEIJE de l'INRIA Sophia Antipolis, et plus
particulièrement en collaboration avec Roberto Amadio.
Ces actions vont constituer une aide primordiale à la réalisation de notre objectif plus spécifique qu'est la définition d'un langage C++//. Tout d'abord, la formalisation d'Eiffel// nous apportant une connaissance et une vision plus précise de la programmation à objets parallèle, elle sera très utile à la définition des primitives et principes de C++//. D'autre part, la réutilisation et les transformations sont indispensables à la réalisation d'un environnement réellement générique de simulation parallèle. Il sera donc important d'en avoir une connaissance et une modélisation formelles. Bien sûr celle-ci sera en Eiffel// et nous appréhendons quelque peu le passage à C++, avec en particulier le traitement très peu dissocié des références et des pointeurs. Mais dans ce contexte, disposer d'une base formelle est sans doute encore plus nécessaire.