Projet IMAG 2003  INCA : Interfaces pour le Calcul Formel

Résumé du projet

 Le logiciel en calcul formel a été longtemps dominé par des systèmes généralistes tels que Axiom, Maple et Mathematica. Désormais, dans un but d'efficacité et de réutilisation de code, apparaissent des bibliothèques spécialisées, comme la bibliothèque LinBox pour l'algèbre linéaire exacte.

 

 Notre premier objectif est de structurer le code de la bibliothèque LinBox, afin de faire interagir efficacement et simplement plusieurs modules. En pratique, cela consiste à identifier des composants communs à plusieurs modules, puis à formaliser ces composants et leurs relations de dépendance, ce qui fournira les interfaces au niveau de la conception de la bibliothèque. Ces interfaces de conception seront exprimées dans un cadre diagrammatique.

 

 Notre second objectif est d’améliorer la convivialité de ces modules, en fournissant à l’utilisateur des interfaces compatibles avec le langage mathématique qui lui est habituel. Ce petit langage d’interfaces pour l’utilisateur sera développé à partir de la formalisation diagrammatique réalisée dans la première partie du projet. Il devra préserver  l’efficacité du code.

 

 Ce projet concerne le calcul formel et le génie logiciel. Il se situe donc à l'interface mathématique-informatique, et à ce titre il relève de plusieurs des axes stratégiques de recherche de l'IMAG: modélisation et calcul, logiciels et systèmes, mathématiques et logiques pour l'informatique.

 

 Ce projet vise à réconcilier efficacité et modularité, ce qui constitue un problème crucial du calcul formel, qui a souvent été abordé sous l'angle des types abstraits de données. L'approche diagrammatique utilisée ici est nouvelle et beaucoup plus puissante. Le projet constitue aussi un banc d'expérimentation pour ces techniques diagrammatiques en génie logiciel.


Table des matières :


Mots clés :  Calcul Formel, Génie Logiciel

 

Contact officiel :  Mme Dominique DUVAL

  Organisme : Laboratoire de Modélisation et Calcul

  Fonction : Professeure Université Joseph Fourier

  Adresse : IMAG-LMC, B.P. 53, 38041 GRENOBLE cedex 9

  Tél : (33) 4 76 51 46 05                                  Fax :  (33) 4 76 63 12 63

  Mél : Dominique.Duval@imag.fr

 

Fournitures

 

Démonstrateur

· Valider l’approche diagrammatique sur un module de la bibliothèque LinBox.

 

Mars 2004

Interfaces de conception

· Structurer le code de la bibliothèque.
·  Développer les spécifications diagrammatiques pour prendre en compte l’approche objet.

 

Mars 2005

Interfaces de bibliothèque

·   Améliorer la convivialité des modules.

 

Mars 2005

 

 

Titre du Projet : Projet INCA : Interfaces pour le calcul formel.

Responsable du projet : Dominique DUVAL – Professeure UJF, Laboratoire de Modélisation et Calcul (Directeur : G.-H. Cottet)

Participants au projet :

 

Présentation du contexte

 

Le logiciel en calcul formel a été longtemps dominé par des systèmes généralistes tels que Axiom, Maple Mathematica. Matlab est un système numérique aux fonctionnalités voisines. Ces systèmes sont convaincants, ils ont eu un impact substantiel. Il est aussi cependant bien connu qu'ils ont leurs limites s'il s'agit de développer des modules

logiciels de hautes-performances, sûrs et pouvant être utilisés comme composants d'autres ensembles. Pour participer en calcul formel à la démarche de réutilisation de code en calcul scientifique, l'objectif de bibliothèques comme LinBox[1] (pour l'algèbre linéaire exacte), Synaps[2] ou MPsolve (pour les polynômes), Givaro[3] (pour les corps finis), NTL[4] (pour la théorie des nombres), GMP et MPfr pour l'arithmétique en précision arbitraire etc. est de fournir de tels modules logiciels symboliques dans des domaines fondamentaux du calcul formel.

Des contributions sont possibles en analyse numérique en termes de méthodes hybrides symboliques-numériques et de préconditionnements aléatoires par exemple, à l'aide des bibliothèques de type BLAS, LAPACK.

La période est propice à l'élaboration de solutions pour répondre à une forte demande en efficacité et en réutilisation de code pour une plate-forme d'expérimentation dans le domaine. Une littérature importante a été produite ces quinze dernières années en algorithmique exacte. Il y a aussi eu des écritures de prototypes par exemple dans LinBox néanmoins sans effort systématique pour rendre les acquis directement accessibles aux utilisateurs. Récemment, un groupe de travail s'est organisé autour des outils de calcul formel libre (l'effort collaboratif Roxane[5] en C/C++), afin d'essayer d'organiser les ressources pour les rendre plus facilement interopérables.

 

Par ailleurs, dans le cadre du génie logiciel, l'accroissement de la taille et de la complexité des composants a engendré un regain d'intérêt pour les techniques formelles de conception, de vérification et de preuve :  on peut citer le projet CASL pour les spécifications, les systèmes Coq, B et VDM pour des preuves.

Les méthodes diagrammatiques sont largement utilisées pour une modélisation semi-formelle, par exemple via le langage UML. D'un point de vue plus formel, ces techniques diagrammatiques sont très récentes en génie logiciel, elles reposent sur une utilisation systématique des esquisses projectives au niveau de la méta-spécification. Mais par ailleurs elles sont voisines de la théorie des catégories, qui forme le langage habituel de structuration des mathématiciens. C’est pourquoi ces méthodes devraient s’avérer bien adaptées à la fois aux interfaces de conception (entre différents modules C++) et aux interfaces d’utilisation (entre la bibliothèque et ses utilisateurs).

Un exemple détaillé : la résolution exacte de systèmes linéaires=

·        Position du problème de design

En calcul formel, les méthodes itératives pour résoudre un système linéaire de type A x = b ne dépendent pas de la structure de la matrice A. Celle-ci peut être creuse quelconque, structurée, bande, Hankel/Toepliz, ou même dense. Il s’en suit que ces algorithmes peuvent s'écrire indépendamment de cette structure. Ainsi, dans Linbox, cet ensemble de boîtes noires est représenté par différentes classes ayant toute un seul point commun : une méthode commune Apply qui effectue le produit de la matrice par un vecteur. Ensuite, chacun des algorithmes itératif (résolution de système, mais aussi, polynôme minimal, rang, déterminant, etc.) utilise de manière générique exclusivement cette méthode. En C++, une telle classe s'écrira par exemple de la manière suivante :

class
MaBoiteNoire {
...
int[] Apply(int[]) ;
}

 

C'est là que les problèmes commencent. En effet, tout d'abord et pour des raisons d'efficacité, c’est le langage C++ qui a été choisi.  En Java, Aldor ou peut-être Haskell par exemple, l'écriture des structures mathématiques aurait pu éventuellement être plus simple. Malheureusement, nous avons besoin des méthodes les plus efficaces possibles pour pouvoir traiter les problèmes les plus grands possibles. Ceci posé, nous essayons en outre d'avoir un certain nombre des caractéristiques suivantes :

1.       Le choix du vecteur doit être laissé à l'algorithme. Ainsi, celui-ci peut utiliser les vecteurs de la librairie standard, des colonnes de matrices, des vecteurs creux, etc. Ceci est indispensable, afin de permettre aux algorithmes d'être le plus efficaces possible.

2.       Les matrices doivent pouvoir elle-même être des blocs de matrices de plus haut niveau.

3.       Dans le cadre d'une utilisation par interface au travers d'un logiciel, l'ensemble des possibilités de la bibliothèque risquent d'être pécompilées. La multiplication des solutions possibles à tous les niveaux (algorithme, matrice, vecteurs, polynômes, corps de base, etc.) produit alors une explosion de code exécutable. Nous essayerons si possible de réduire cette production.

 

En C++, le premier point peut être résolu simplement par l'utilisation de template. Ainsi, le type de vecteur peut être spécifié seulement à l'appel :

 

class
MaBoiteNoire {
...
  template<class Vecteur> Vecteur Apply(Vecteur) ;
}

 

Pour le second point, le problème est qu'il faudrait que toutes les boîtes noires soient du même type. Alors, il faut qu'elles héritent d'une classe abstraite commune :

 

class
MaBoiteNoire : public BBAbstraite {
...
int[]  Apply(int[]);
}

 

Cela permet en outre la résolution du troisième point, si les algorithmes ne s'instancient que sur cette classe abstraite.

 

Malheureusement, il est conceptuellement impossible d'avoir une classe abstraite avec une méthode template ! En effet, le mécanisme de table virtuelle ne peut résoudre l'appel de la méthode abstraite puisqu'il ne connaît pas l'instance exacte de cette méthode (le vecteur qui sera passé n'est pas connu au moment de l‘affectation).

 

Il serait alors possible de faire remonter le template au niveau de la classe et utiliser l'héritage :

 

template<class Vecteur>
class MaBoiteNoire : public BBAbstraite<Vecteur> {
...
 
Vecteur Apply(Vecteur) ;
}

 

Malheureusement, cette solution replace, en quelque sorte, le choix du vecteur au niveau de la création de la boîte noire. En effet, un algorithme ne pourra utiliser que les vecteurs qui lui seront passés en arguments. Alors, il est bien sûr possible de créer une classe associée à un algorithme décrivant les vecteurs qui seront nécessaires. Seulement cette structure additionnelle doit être reproduite à tous les niveaux algorithmiques. En outre, elle ne peut pas refléter de manière exhaustive les choix dynamiques.

En conclusion, nous n'avons pas de solution totalement satisfaisante : dans Linbox, la première méthode a été choisie, puis la deuxième.

 

Enfin, ce genre de problème, et d'autres , se produisent à tous les niveaux de généricité (algorithmes, matrices, polynôme, vecteurs, corps de base etc.) et celui des boîtes noires semble le plus facile. Par exemple, depuis la création de Axiom/Aldor, les spécifications d'un corps fini ont évolué et nous connaissons maintenant une bonne façon de spécifier la notion de non-divisibilité par zéro.  

·        Une idée : utiliser les spécifications

 

En effet, pour résoudre chacun des problèmes, nous avons considéré pour l'instant chaque couche l'une après l'autre. L'idée, ici, est de s'abstraire un peu plus et d'essayer d'obtenir une vision globale du problème par l'intermédiaire des spécifications. Dans ce cadre, une autre vision peut émerger. Voici par exemple une ébauche de spécifications que nous pouvons obtenir pour les deux précédentes approche de codage des boites noires :

Zone de Texte:
class
MaBoiteNoire {
...
  template<class Vecteur> Vecteur Apply(Vecteur) ;
}


Ici, les boites sont distinctes et peuvent utiliser de manière générique plusieurs types de vecteurs.


Zone de Texte:
class MaBoiteNoire :
public BBAbstraite {
...
int[]  Apply(int[]);
}

Dans ce cas, au contraire, les matrices héritent toutes d’une même classe, mais ne peuvent alors pas être générique par rapport au type de vecteur.

Pour le problème des boîtes noires, nous pouvons construire une première vision abstraite du produit matrice-vecteur, comme étant une loi de composition entre une spécification des boites noires B et une spécification des vecteurs V, de la manière suivante :

Ici, les nœuds correspondent à des spécifications de plus en plus précises. Et les flèches à un enrichissement successif de ces spécifications (morphismes).

Pour résumé, l’idée est tout d’utiliser des spécifications pour analyser les problèmes de conception, cela donnera alors :

1.       une vision plus globale et plus abstraite

2.       de nouvelles pistes de conception

L’espoir étant que ces nouvelles pistes seront meilleures car les spécifications sont plus proches de la programmation que ne l'est le cadre mathématique ensembliste utilisé jusqu’à présent dans LinBox. Le but étant alors d’écrire chaque algorithme à son meilleur niveau de généricité.

Enfin, ces spécifications peuvent en outre être réutilisée pour résoudre les problèmes d'interface pour les utilisateurs de la bibliothèque. En effet, au niveau de la conception,  les morphismes de spécifications formalisent les dépendances entre les composantes et au niveau utilisateur, les modèles des spécifications fournissent le point de vue ensembliste qui permet de déduire un petit langage d’interfaces utilisables par un mathématicien.

 

Présentation des objectifs et de l'approche scientifique

Dans ce cadre, notre objectif est triple :

·        D’une part, identifier des composants atomiques de la bibliothèque LinBox (cela peut être par exemple les notions de matrice structurée ou non, de polynôme, de vecteur et d'espace vectoriel, de corps ou d'anneau de base pour l'arithmétique, ou encore l'échange de données binaires entre systèmes) et les organiser en catégories, domaines, etc. afin de bien analyser les relations entre ces composants. Ceci doit permettre de définir quelles interfaces de conception sont intéressantes. Ces interfaces devront être associées à des objets C++ à part entière, afin de préserver l’efficacité des modules. L'approche formelle diagrammatique pourra jouer un rôle unificateur et permettra d’aborder les différents problèmes de spécification qui ne manqueront pas de se poser. 

·        D’autre part, proposer aux utilisateurs mathématiciens un petit langage d’interface simple à utiliser. Celui-ci devra être  à la fois proche des habitudes des utilisateurs et suffisamment compatible avec la structuration interne des composants logiciels pour ne pas perdre d’efficacité. Ici encore l’approche diagrammatique devrait s’avérer utile, car elle est proche de la théorie des catégories, sur laquelle repose la structuration des objets mathématiques manipulés.

·        Et enfin, dans un cadre plus précisément informatique, développer les spécifications diagrammatiques pour prendre en compte des notions liées à l’approche objet, qui n’ont pas encore été étudiées dans ce formalisme.

Les contraintes sont multiples :

A plus long terme, cette étude des interfaces doit ouvrir la voie vers une programmation générique de plus haut niveau qu'actuellement, et une utilisation aisée dans les logiciels génériques de routines spécialisées et efficaces. Ceci est réalisé dans des bibliothèques comme Linbox ou Synaps pour Maple et pourra être facilement généralisé à partir des interfaces et d'un protocole d'échange de données (voir par exemple UDX[6]).

Ce projet doit aider à organiser les connaissances mathématiques nécessaires au calcul formel de façon à la fois rigoureuse et efficace. Les problèmes de généricité sont cruciaux, leur résolution ne doit pas affaiblir l'efficacité des algorithmes. Les buts poursuivis intéressent le calcul formel en général. Cependant le problème est très difficile, et c’est pour des raisons de réalisme que ce projet se limite volontairement à la bibliothèque LinBox, spécialisée dans l’algèbre linéaire exacte. La formalisation des interfaces, au niveau de conception et au niveau d’utilisation, doit permettre de faire le lien entre le point de vue abstrait et dénotationnel des notions mathématiques mises en jeu (corps, polynômes, matrices, nombres algébriques, etc.) et le point de vue concret et opérationnel des implantations en C++.  La puissance et la simplicité conceptuelle de l’approche diagrammatique devraient permettre de conjuguer la rigueur et l'efficacité souhaitées.

Les missions prévues dans le cadre du projet visent à renforcer nos relations avec la communauté scientifique internationale concernée par ces recherches : réunions du projet LinBox, congrès internationaux de calcul formel, réunions du groupe IFIP « Foundations of System Specifications », etc.
Les vacations nous permettront de proposer des stages pour l’écriture et les tests de prototypes.

Evaluation du risque et indicateurs de succès

Les risques de ce projet sont de nature scientifique et technologique.
Ce projet devrait déboucher sur :

Quelques repères bibliographiques 

J.G. Dumas, T. Gautier, M. Giesbrecht, P. Giorgi, B. Hovinen, E. Kaltofen, B. D. Saunders, W. J. Turner, G. Villard. LinBox: A Generic Library for Exact Linear Algebra. International Congress of Mathematical Software, (2002), Beijing.

D. Duval, C. Lair. Diagrammatic Specifications. Mathematical Structures in Computer Science, à paraître.

D. Duval, J.-C. Reynaud. Sketches and computation (Part I): Basic Definitions and Static Evaluation. Mathematical Structures in Computer Science  4 (1994) 185-238.

D. Duval, J.-C. Reynaud. Sketches and computation (Part II): Dynamic Evaluation and Applications. Mathematical Structures in Computer Science  4 (1994) 239-271.


Publications

Alexandre Vautier. SketchUML-1.0. Septembre 2003.

Alexandre Vautier. Traductions entre diagrammes de Spécifications et diagrammes UML. Mars 2004.

Elyasin Ayadi. Dessiner les Calculs. Octobre 2004.

Jean-Guillaume Dumas, Dominique Duval et Jean-Claude Reynaud. Rapport à mi parcours. Octobre 2004.

Jean-Guillaume Dumas and Dominique Duval.
Towards a diagrammatic modeling of the linbox c++ linear algebra library.
Rapport de recherche, IMAG-CCSD-00012346, ArXiv cs.SC/0510057, October 2005.

Dominique Duval, Christian Lair, Catherine Oriat, and Jean-Claude Reynaud.
A zooming process for specifications, with an application to exceptions.
Rapport de recherche, IMAG-LMC 1055 I, 2003.

Dominique Duval and Jean-Claude Reynaud.
Diagrammatic logic and effects : the example of exceptions.
Rapport de recherche, IMAG-CCSD-00004129, February 2005


Dominique Duval and Jean-Claude Reynaud.
Diagrammatic logic and exceptions: an introduction.
In Mathematics, Algorithms, Proofs, Schloss Dagstuhl, Germany, January 9-14, 2005, January 2005.

Logiciels

SketchUML-1.0

DessinerLesCalculs



[1] LinBox : bibliothèque générique pour l'algèbre linéaire semi-numérique. http://www.linalg.net.

[2] Synaps : SYmbolic Numeric ApplicationS. http://www-sop.inria.fr/galaad/logiciels/synaps.

[3] Givaro : bibliothèque C++ pour l'arithmétique efficace dans les corps finis. http://www-id.imag.fr/Logiciels/givaro.

[4] NTL : a Library for doing Number Theory. http://www.shoup.net/ntl.

[5] Roxane : Reliable Open Software-Components for Algebraic and Numeric Efficiency. http://www-sop.inria.fr/galaad/logiciels/roxane.

[6] UDX : Universal Data Exchange. http://www.loria.fr/~rouillie/Soft/UDX/www.