The Centaur System - Deriving Programming Environments from Abstract Specifications
by Valérie Pascual
Formal descriptions of programming languages can serve as the input to programming environment generators that integrate a variety of tools to develop and maintain programs in a safe manner. The Centaur system, developed between 1986 and 1993 in the ESPRIT projects GIPE and GIPEII in a collaboration between INRIA, CWI, University of Amsterdam, Gipsi S.A., Linköping University, PTT Research, SEMA Group and Technologische Universität Darmstadt and distributed by the CROAP team at INRIA Sophia-Antipolis is a successful example of such a programming environment generators.
For most practical purposes, programs can be viewed as tree-like data structures, where each expression contains a number of sub-expressions and so on recursively. In the framework of two esprit projects (GIPE and GIPE II), the CROAP project has developed in collaboration with other research institutions from all over Europe, a programming environment generator, Centaur, where all tools revolve around a central tree processing module. This programming environment makes it possible to construct a variety of tools for a given language, based on a formal description of this language.
The first formal description is the tree language. In the same way that a programs in a programming language must respect a precise set of syntax rules, the trees that represent these programs should also respect a set of rules, which we usually call abstract syntax rules. Once the tree language is described, it important to describe the relation the abstract syntax on trees and the concrete syntax on texts. This can be achieved using a parsing specification to describe how written texts can be transformed into tree structures and a pretty printing specification to describe how trees can be rendered in a text whose layout respects the program structure. A variety of programming tools can automatically be derived from these specifications: syntax-aware editors, program beautifiers, menu-directed program transformation tools, which propose only syntactically correct program transformations to the user.
The Centaur programming environment also provides means to describe the semantics of programming languages. The formalism of Natural Semantics makes it possible to view various properties of programming languages, like the type discipline or the behavior of programs as logical systems. With this model, checking that a program is well-typed is equivalent to building a proof that the program is well-typed. Drawing on results on proof theory, this approach makes it possible to state formally general properties of programming languages and prove them. This is very useful in today's word, where people want to be ensured that using a specific programming language will reduce the chances of implementation errors.
The logical systems specified using Natural semantics also have the important property that they can be executed, thanks to a Prolog compiler. Thus, the formal specifications can be used directly to check sensitive programs, with no need for further implementation. As Prolog tends to be slower than other programming languages, the CROAP group also studies ways to execute natural semantics through other kinds of execution engines.
The current research in this framework aims at providing tools especially tuned for systematic program transformations. Applications of these tools can be found in all the efforts to maintain and port legacy software, like the year 2000 problem.
To complete the range of available facilities, the Centaur system also incorporates a graphical user interface, communication modules, and a graph display tool.
The Centaur system is the base for industrial tools revolving around the Fortran language, commercialised by Simulog S.A (for more details see http://www.simulog.fr/foresys/). In the CROAP project itself, it is also used in an exhaustive study of the object oriented programming languages Eiffel and Java.
Details about Centaur and the conditions of availability can be found at: http://www.inria.fr/croap/centaur/centaur.html
Please contact:
Valérie Pascual
Tel: +33 4 9365 7806
E-mail: Valerie.Pascual@inria.fr
