Skip to main content

1990 | Buch

Specification and Transformation of Programs

A Formal Approach to Software Development

verfasst von: Helmut A. Partsch

Verlag: Springer Berlin Heidelberg

Buchreihe : Monographs in Computer Science

insite
SUCHEN

Über dieses Buch

"Specification and transformation of programs" is short for a methodology of software development where, from a formal specification of a problem to be solved, programs correctly solving that problem are constructed by stepwise application of formal, semantics-preserving transformation rules. The approach considers programming as a formal activity. Consequently, it requires some mathematical maturity and, above all, the will to try something new. A somewhat experienced programmer or a third- or fourth-year student in computer science should be able to master most of this material - at least, this is the level I have aimed at. This book is primarily intended as a general introductory textbook on transformational methodology. As with any methodology, reading and understanding is necessary but not sufficient. Therefore, most of the chapters contain a set of exercises for practising as homework. Solutions to these exercises exist and can, in principle, be obtained at nominal cost from the author upon request on appropriate letterhead. In addition, the book also can be seen as a comprehensive account of the particular transformational methodology developed within the Munich CIP project.

Inhaltsverzeichnis

Frontmatter
1. Introduction
Abstract
This text is concerned with some problems of software development that are usually dealt with under the heading “software engineering”. However, we entitled this text “specification and transformation of programs — a formal approach to software development” rather than just “software engineering” in order to emphasize from the very beginning that we will only be concerned with some of the technological problems of software engineering and disregard all managerial aspects.
Helmut A. Partsch
2. Requirements Engineering
Abstract
In Sect. 1.3, we introduced requirements engineering as that phase in the software development process where vaguely defined, little detailed user wishes are to be made into a more precise, though still little detailed specification of the problem to be solved. Moreover, we also aimed at a formal problem specification as the result of the requirements engineering phase. For the present chapter, however, in order to establish the relation to traditional software engineering, we will start with a somewhat broader view and consider formality as a desirable, but not mandatory objective. This means in particular that we are also going to give a short account on the state of the art in traditional requirements engineering, mainly in order to contrast it (in Chap. 3) with our approach where a precise statement of the user’s wishes in terms of a formal language is aimed at.
Helmut A. Partsch
3. Formal Problem Specification
Abstract
In the previous chapter we surveyed some approaches to requirements engineering in the framework of traditional software engineering. All these approaches aim at providing a formalism for precisely describing a problem to be solved. None of them, however, except for Gist, allows the formulation of a formal problem specification in the (intuitive) sense of Sect. 1.5.
Helmut A. Partsch
4. Basic Transformation Techniques
Abstract
In this chapter we introduce the theoretical foundations of transformational programming together with a variety of simple transformation rules. In the following chapters, these will be considered as a basis for deriving and proving correct further, more advanced, compact rules. Additionally, we will also show that these basic rules together with elementary strategies are already sufficient to do transformational program development for certain specific tasks. The examples will start from formal specifications as developed in Sect. 3.6.
Helmut A. Partsch
5. From Descriptive Specifications to Operational Ones
Abstract
This chapter deals with the problem Given a descriptive problem specification, how many a solution be derived?. since solving this problem needs ideas, experience, and intuition on the developer’s side, it should be clear that it cannot be solved by purely mechanical reasoning.
Helmut A. Partsch
6. Modification of Applicative Programs
Abstract
Applicative programs, irrespective of whether given as an initial operational problem specification or derived using the transformations and tactics dealt with so far, can often be further manipulated. In particular, modifications can be carried out that aim at increasing efficiency by speeding up the performance of certain computations, avoiding duplicated evaluations of expressions, and so on. Most of these manipulations could also be done later in the development, say on a procedural level. However, experience (see for example [Burstall, Darlington 77] and [Pepper, Partsch 80]) has shown that it is advisable to do these manipulations on the applicative level as far as possible, thus profiting from the obvious advantages (such as ‘referential transparency’ [Quine 60]) of this level of formulation. Thus, for example, all techniques that in a procedural environment are referred to as ‘loop fusion’ are covered in an applicative scenario by the much more general techniques for merging of computations (see below).
Helmut A. Partsch
7. Transformation of Procedural Programs
Abstract
In the previous chapters, it has been mentioned several times that the major part of any program development by transformations can be done at the level of applicative formulations. Nevertheless, when aiming at the efficient running of programs on conventional von Neumann machines, a few more transformations have to be available for introducing variables (the key concept of the von Neumann machine) together with related constructs such as assignment, iteration, and loops. In contrast to the transformations dealt with in earlier sections, these rules are of a much more mechanical nature. One can thus imagine that they might be performed automatically, for example by a suitable optimizing compiler. Since the whole subject, sometimes called ‘optimizing transformations’, is extensively treated in standard textbooks on compiler construction and also in [Bauer, Wössner 82] or [Illsley 88], our treatment here will be a little sketchy and by no means comprehensive. Still, it suffices to give at least a rough impression of what these rules are about.
Helmut A. Partsch
8. Transformation of Data Structures
Abstract
A program development typically starts with a formal specification (of an abstract program) based on some suitably defined abstract type (or a hierarchy of types). In the course of developing a program by transforming the control constructs (using the techniques introduced in the previous chapters) a situation will be reached where a further successful development is subject to an appropriate change of the data structures involved.
Helmut A. Partsch
9. Complete Examples
Abstract
In the previous chapters a lot of examples have been given to illustrate various transformation rules and strategies. The emphasis there was on demonstrating different (individual) techniques in the overall software development process, for example the transition from descriptive to operational specifications or improvement of applicative programs. Certain problems have been considered in various stages scattered over different chapters. Except for the queens problem of Sect. 1.6, however, there were no complete treatments of problems leading from an informal problem statement to an efficient procedural program. Therefore, in this chapter, a couple of further examples will be considered in a more complete way.
Helmut A. Partsch
Backmatter
Metadaten
Titel
Specification and Transformation of Programs
verfasst von
Helmut A. Partsch
Copyright-Jahr
1990
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-61512-2
Print ISBN
978-3-540-52589-9
DOI
https://doi.org/10.1007/978-3-642-61512-2