Abstract FR:

Dans le cadre du developpement formel de programmes (specifications, raffinages, transformations), nous construisons un atelier de calcul symbolique. Cet atelier (arcs) est bati pour supporter des methodes de developpement formel de programmes a partir de specifications. Il vise le monde de la recherche en genie logiciel. Il est destine a assister la conception de methodes de programmation en fournissant un environnement de developpement specifique des lors que les langages et regles des methodes sont definis formellement. Le noyau de l'environnement ainsi fourni est constitue d'un editeur interactif et graphique de termes algebriques ou logiques et des outils de traitement de ces derniers. Les services proposes par l'atelier se font au plus haut niveau d'abstraction possible: celui de la syntaxe abstraite. Les traitements sont exprimes par des schemas de reecriture et constituent des parametres de travail. Pour garantir la liberte d'expression et la mobilite des frontieres du systeme, les langages, symbolismes et regles des methodes sont des parametres modifiables et non des constituants predefinis. La visualisation est en deux dimensions pour permettre l'usage de symboles graphiques tels que ceux utilises en mathematique et de plus en plus pour les formalisations en informatique , l'edition d'expressions graphiques complexes, et la manipulation directe par designation de ces dernieres a la souris. Une approche de formalisation est elaboree pour specifier le comportement operationnel du systeme arcs en particulier et des systemes interactifs et graphiques en general. De nombreuses experimentations sont faites avec arcs: edition multiformalisme, manipulation de termes algebriques, transformations par schemas de reecriture, decompilation, etc. . .