ESPRIT Project PROSPECTRA

PROgram development by SPECification and TRAnsformation

In the methodology of PROgram development by SPECification and TRAnsformation, algebraic specifications are the basis for constructing correct and efficient programs by gradual transformation. The combination of algebraic specification and functionals increases abstraction, reduces development effort, and allows reasoning about correctness and direct optimisations. The uniformity of the approach to program and meta-program development is stressed.

Preface of [HK 93]:

The PROSPECTRA project has been partially funded by the Commission of the European Communities under the ESPRIT Programme, ref. #390 and #835, from March 1985 to March 1990. Many people have contributed to the project (see The PROSPECTRA Consortium and The PROSPECTRA Teams). The Consortium also very gratefully acknowledges the constructive contributions of the project officers from the Commission for PROSPECTRA, Dr. Pierre-Yves Cunin and Jack Metthey, and, last not least, the Reviewers, Robert F. Maddock (IBM, Hursley), Professor Peter Pepper (Technische Uni-versität Berlin), and Professor John Darlington (Imperial College, London), who have carefully, critically and benevolently guided the project through easy and hard times.

The objective of this documentation is a coherent presentation of the outcome of the project PROSPECTRA ("PROgram development by SPECification and TRAnsformation") that aimed to provide a rigorous methodology for developing correct software and a comprehensive support system. The results are substantial: a theoretically well-founded methodology covering the whole development cycle, a very high-level specification and transformation language family allowing meta-program development and formalisation of the development process itself, and a prototype development system supporting structure editing, incremental static-semantic checking, interactive, context-sensitive transformation and verification, development of transformation (meta-) programs, version management, etc., with an initial library of some specifications and a sizable collection of implemented transformations.

One intended audience for this documentation is clearly the academic community working in the areas of Formal Methods for software (and hardware) development, Specification Languages, Theory of Compu-tation, Semantics and Verification, implementation of Functional Languages, Structure Editors, Attribute Grammars, advanced Software Engineering Environments, etc. Of even more importance is the industrial community interested in the use of Formal Methods. It is still a long way to the widespread use of production-quality systems employing Formal Methods to increase correctness, reliability, and safety of systems, and productivity of developers. The PROSPECTRA Consortium has made a conscious effort of technology transfer, trying to implement the state-of-the-art, in a realistic setting. The prototype system, a "PROSPECTRA workstation", allows serious experimentation to enable feedback for extensions and improvements (that are undoubtably needed). Eventually, we see various classes of PROSPECTRA users, with potentially distinct abilities and educational background: the PROSPECTRA system developers, the developers of transformations and development methods, the developers of (generically re-usable) specifications, and the software developers (end users). At the moment, the system is really only usable externally for benevolent experimentors due to its size and complexity of integration (coming from many development sites). We hope for a new version in the near future, however, based on the extensive experience with PROSPECTRA, as related work at Universität Bremen is presently funded by the Bundesministerium für Forschung und Technologie in the national project KORSO ("Korrekte Software").

This volume contains three Parts. Part I contains a description of the PROSPECTRA Methodology of specification, transformation and verification, including the catalogue of presently available transformations. Part II contains a description of the PROSPECTRA Language Family: a rationale for the language subsets and their relationship, reference manuals for concrete syntax, informal semantics, abstract syntax and static semantic attributes, and a formal definition of the semantics of the specification subset. Part III contains a description of the PROSPECTRA System: a rationale for the uniform system structure, a short overall users guide, and reference manuals for the various system components.

The PROSPECTRA Consortium

The PROSPECTRA Teams

General Publications