Méthodes formelles pour les objets

De nombreux modeles formels a objets ont ete proposes au cours de la periode ecoulee. Aux extensions a objets de theories existantes (logiques, categories, lambda calcul, specifications algebriques ou basees sur les etats (Z, VDM) se sont ajoutes des calculs d'objets, notamment pour les acteurs et, plus recemment, pour les agents mobiles. Les concepteurs d'outils de developpement disposent maintenant d'un ensemble fourni de theories pour formaliser les systemes a objets. Mais ces theories sont souvent disparates, car elles reposent sur des definitions specifiques et incompatibles des objets. Leur usage est encore restreint, car leur mise en oeuvre est lourde et couteuse, ou les modeles sont trop specifiques, ou ils ne correspondent pas a la pratique des developpeurs.

Une tendance actuelle est l'application pratique, meme partielle, de cette recherche < fondamentale >. L'objectif est d'assister l'analyste dans l'ecriture et la preuve des proprietes attendues du systeme, le concepteur dans l'expression des composants ou des architectures de composants (patrons de conception) et le programmeur dans la verification de proprietes statiques ou dynamiques de l'application developpee. Ce numero special de la revue L'objet, consacre aux methodes formelles pour les systemes a objets, illustre cette tendance.

Le premier article, de S. Dupuy, Y Ledru et M. Chabre-Peccoud, traite d'outils d'analyse qui donnent une semantique aux modeles semi-formels qu'on retrouve dans beaucoup de developpements industriels. Les auteurs repondent au besoin d'une semantique formelle pour UML en se basant sur la notation Z Ainsi, un sens precis est donne a chaque concept des diagrammes de classes et d'objets d'UML. Le travail de groupe est facilite car les ambigu?tes, source de discussions, sont fortement reduites. La semantique permet de controler des proprietes de la specification et de construire des outils d'assistance automatises. Les deux articles suivants concernent l'ajout de formalisme dans la description de composants reutilisables. La formalisation a des effets benefiques sur la documentation (base de la reutilisation), la recherche (appariement), l'organisation de la bibliotheque (criteres de structuration). Ainsi, l'article dA. Mikhajlova vise a specifier formellement des composants et leurs relations dans une bibliotheque, y compris des mecanismes de bas niveau. La technique utilisee est suffisamment abstraite (constructions non deterministes, lambda calcul) et formelle pour decrire le fonctionnement precis des classes et verifier que leur implementation est correcte. L'approche est illustree sur des classes de collections de la bibliotheque Java. L'article de H. -A. Jacobsen et B. J. Kramer concerne l'annotation de specifications IDL (CORBA) par des assertions logiques et des contraintes de synchronisation. IDL est un langage normalise commun aux differents langages de programmation a objets qui permet l'interoperabilite d'objets heterogenes distants. Les annotations proposees enrichissent le langage IDL sans le denaturer Les auteurs explorent aussi les formes possibles d'integration de ces contraintes dans IDL, avec des patrons de conception.

Le quatrieme article est plus proche des preoccupations de programmation et se situe au niveau des modeles formels a objets. Il traite du typage statique dans les langages d'acteurs. Le controle de type est une technique essentielle en verification de programmes. En ce qui concerne la programmation sequentielle (imperative ou fonctionnelle), de nombreux travaux de recherche ont mis en evidence les problemes de semantique de l'heritage et du sous-typage. En programmation concurrente, le controle de type est plus delicat, car les acteurs peuvent changer dynamiquement et radicalement de comportement, et l'ordre des envois de message n'est pas deterministe. L'article de E Dagnat, M. Pantel, M. Colin et P Salle est une bonne illustration de cette approche.

Nous sommes tres conscients que ces quatre articles, selectionnes sur la vingtaine d'articles soumis, ne couvrent que tres partiellement le vaste domaine des methodes formelles et des objets, mais ils renvoient a des considerations pragmatiques. Ce numero special a beneficie du travail scientifique et technique des membres du comite de lecture qui etait compose de Pascal Andre (IRIN et INPHB), Isabelle Attali (INRIA, Sophia Antipolis), Veronique Benzaken (LRI, Orsay), Didier Buchs (EPFL, Lausanne), Giuseppe Castagna (LIENS, Paris), Michel Dao (CNET, Paris), Kevin Lano (Imperial College, Londres), Roger Rousseau (I3S, Sophia Antipolis) et Graeme Smith (SVRC, Brisbane). Nous remercions aussi les relecteurs qui ont fourni des avis precieux: Michel Allemand, Charles Andre, Christian Attiogbe, Gerard Boudol, Philippe Collet, Roland Ducournau, Jean-Marc Geib, Henri Habrias, Pascal Poizat, Antonio Ravara et Jean-Claude Royer