1990 • 507 Pages • 24.5 MB • English

Posted April 14, 2020 • Uploaded
by bauch.horacio

PREVIEW PDF

Page 1

Texts and Monographs in Computer Science Editor David Gries Advisory Board F. L. Bauer S.D.Brookes C. E. Leiserson M.Sipser

Page 2

Helmut A. Partsch Specification and Transformation of Programs A Formal Approach to Software Development Springer-Verlag Berlin Heidelberg New York London Paris Tokyo Hong Kong

Page 3

Author Helmut A. Partsch Department of Computer Science Faculty for Mathematics and Informatics Catholic University of Nijmegen Toernooiveld 1, 6525 ED Nijmegen, The Netherlands Series Editor David Gries Department of Computer Science, Cornell University Ithaca, NY 14853, USA ISBN-13:978-3-540-52589-9 e-ISBN-13:978-3-642-61512-2 001: 10.1007/978-3-642-61512-2 Library of Congress Cataloging-in-Publication Data Partsch. Helmut A., 1950- . - Specification and transformation of programs: a formal approach to software development/Helmut A. Partsch. p. cm. - (Texts and monographs in computer science) Includes bibliographical references. ISBN-13:978-3-540-52589-9 1. Computer software - Development. I. Title. II. Series. QA76.76.D47P37 1990 005.1-- dc20 90-9553 This work is subject to copyright. All rights are reserved, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broad- casting, reproduction on microfilms or in other ways, and storage in data banks. Duplication of this publication or parts thereof is only permitted under the provisions of the German Copyright Law of September 9, 1965, in its current version, and a copyright fee must always be paid. Violations fall under the prosecution act of the German Copyright Law. © Springer-Verlag Berlin Heidelberg 1990 Softcover reprint of the hardcover 1st edition 1990 The use of registered names, trademarks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regula- tions and therefore free for general use. 2145/3140 - 5 4 3 21 0 - Printed on acid-free paper

Page 4

Preface "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. As such, it is to be considered as a companion and a completion of previously published books on this project, notably [Bauer Wossner 82], [Bauer et al. 85], and [Bauer et al. 87]. Links to these books are provided by cross-references whenever appropriate. This background also influenced the decision to use the language CIP-L as defined in [Bauer et al. 85] and not to experiment with new notation. Even more important was the fact that CIP-L is one of the very few languages with a formal definition of their semantics. Formal semantics is an indispensable prerequisite for transformational programming as a formally based activity. However, most of the technical information contained in this book is easily transferable to almost everyone's pet language and notation. The Organization of the Book The contents of the book attempt to reflect the essential steps in a sequential process of software development from the "problem" to the "machine", i.e. from an informally stated problem, via a formal problem specification, to a final, efficient program. Chapter 1, the introduction, motivates, on the basis of traditional software engineering, the need for new, more formally based approaches in the area of software development. It outlines the basic idea of formal specification and

Page 5

VI Preface transformational programming, explains our particular view of this new paradigm, and relates it to some other modem approaches in programming methodology. An introductory example, spanning the wide range between an informally formulated problem and an efficient program, is intended to convey a fIrst impression of the methodology . Chapter 2 is an excursion. It gives a brief overview of the major problems and currently used approaches in the area of requirements engineering. The need for this kind of background information to be contrasted with our approach became apparent while lecturing on the subject of this book. Someone basically familiar with the subject, or not interested in it, is advised simply to skip the chapter. Chapters 3 to 8 form the heart of this book. Chapter 3 deals with different aspects of formal specifIcation. Apart from some ideas on how to convert an informally stated problem into an adequate, formal specification, it mainly introduces various language constructs for formal specifIcation. These include algebraic types and well-known applicative concepts, but also further constructs specifically tailored to specifying problems rather than programs. The combined use of these constructs is illustrated by a collection of examples most of which reappear as starting points for transformational developments within the following chapters. Chapter 4 introduces our basis for transformational programming. The theoretical foundation of the approach is outlined and a large collection of elementary transformation rules is given. Chapter 5 deals with the problem of how to transform a (non-operational) formal problem description into a fIrst (operational) solution to the problem. Within the framework of a general strategy, lots of individual techniques for mastering this important step are discussed. Particular attention is paid to the interaction between formal, mechanizable steps and human creativity. Chapter 6 is devoted to the improvement of applicative programs. Different classes of techniques are dealt with such as merging of computations, inversion of the flow of computation, storing values rather than recomputing, or computation in advance. SimplifIcation of recursion, as a preparatory step for a subsequent transition to an imperative program, is also discussed. Chapter 7 elaborates on the transition from applicative to imperative programs. As this is a meanwhile well understood area, only a few, representative techniques are given. Furthermore, this chapter also contains a few transformation rules for imperative constructs, to be used mainly for "polishing" the fInal result of a transformational development Chapter 8 raises the topic of data type transformation. Various techniques for correctly implementing algebraic types are discussed as well as the important issue of joint development of control and data structure. Chapter 9 gives a few more advanced examples. Whereas in the previous chapters the emphasis was on the transformational techniques with the examples being used for demonstration purposes, here the emphasis is on the problems themselves and how to solve them by means of our proposed methodology.

Page 6

VII Acknowledgements Those familiar with the Munich CIP project will find its influence throughout this book. Many of the ideas in this book originated and have been developed within the CIP group. Particular thanks are therefore due to F.L. Bauer and the late K. Samelson who have been the driving forces of the project, as well as to all colleagues from the former CIP group. Not just by accident, the title of this book coincides with the title of our ongoing Dutch national project STOP, sponsored by NFI/NWO. It is hardly necessary to mention that research within this project also influenced the manuscript My previous work, which forms the basis of this manuscript, has also benefited a lot from discussions within IFIP Working Group 2.1 ("Algorithmic Languages and Calculi") over the last decade. Hence, thanks to all members of WG 2.1. I am particularly grateful to Frank Stomp, who read nearly all previous drafts of this manuscript and gave lots of technical and stylistic suggestions for almost every paragraph. A number of colleagues have given me substantial constructive criticism on all or parts of this manuscript. For their help I would like to thank Eerke Boiten, Dick Carpenter, Herbert Ehler, Niek van Diepen, Kees Koster, Erik Meijer, Bernhard Moller, and Norbert Volker. Thanks are also due to the students of my course "Programmatuurkunde" at Nijmegen University who have been the "guinea pigs" over the last years. Valuable feedback was also provided by students of ESLAI at Buenos Aires when lecturing on the topic of this book, as well as by students from Technical University of Munich and University of Erlangen. Particular thanks go to Joanna Volker who substantially improved many of the English formulations, and Greta LOw who did an excellent job in preparing the fmal camera-ready form. I am also grateful to David Gries who accepted the manuscript for publication in this series and to Hans Wossner, friend and colleague in the CIP project from the beginning, and his team of Springer-Verlag for their valuable advice in preparing the book. Finally, I thank my wife, Uschi, and son, Stefan, for their love and patience while I was writing this book. Kleve, Spring 1990 H. Partsch

Page 7

Contents 1. Introduction ....................................................................... 1 1.1 Software Engineering ....................................................... 1 1.2 The Problematics of Software Development ............................. 4 1.3 Formal Specification and Program Transformation ..................... 6 1.4 Our Particular View of Transformational Programming ................ 11 1.5 Relation to Other Approaches to Programming Methodology. . .. . .. . .. 12 1.6 An Introductory Example ................................................... 15 2. Requirements Engineering ................................................... 19 2.1 Introduction... .... ... .. .... ..... .... .. ....... ......... ... ... ..... . .. . .. . .. ... 19 2.1.1 Basic Notions ...................................................... 20 2.1.2 Essential Criteria for Good Requirements Defmitions . . .. . .. 23 2.1. 3 The Particular Role of Formality ................................. 25 2.2 Some Formalisms Used in Requirements Engineering ... ... ... ... ..... 27 2.2.1 A Common Basis for Comparison .............................. 27 2.2.2 Flowcharts.......................................................... 28 2.2.3 Decision Tables.................................................... 29 2.2.4 Formal Languages and Grammars............................... 30 2.2.5 Finite State Mechanisms .......................................... 31 2.2.6 Petri Nets ........................................................... 32 2.2.7 SNSADT ........................................................... 34 2.2.8 PSI)PSA ........................................................... 37 2.2.9 RSL/REVS ......................................................... 40 2.2.10 EPOS ................................................................ 44 2.2.11 Gist.................................................................. 49 2.2.12 Summary ........................................................... 52 3. Formal Problem Specification .............................................. 56 3.1 Specification and Formal Specification ................................... 56 3.2 The Process of Formalization .............................................. 60 3.2.1 Problem Identification ............................................ 60 3.2.2 Problem Description .............................................. 63 3.2.3 Analysis of the Problem Description ............................ 64 3.3 Defmition of Object Classes and Their Basic Operations ............... 65 3.3.1 Algebraic Types ................................................... 65 3.3.2 Further Examples of Basic Algebraic Types ................... 77 3.3.3 Extensions of Basic Types ....................................... 81

Page 8

x Contents 3.3.4 Fonnulation of Concepts as Algebraic Types .................. 84 3.3.5 Modes......... ...................................................... 95 3.4 Additional Language Constructs for Fonnal Specifications ............ 98 3.4.1 Applicative Language Constructs ................................ 100 3.4.2 Quantified Expressions ........................................... 107 3.4.3 Choice and Description ....... ...................... ... ........... 109 3.4.4 Set Comprehension ................................................ 113 3.4.5 Computation Structures........................................... 115 3.5 Structuring and Modularization ............................................ 117 3.6 Examples ..................................................................... 119 3.6.1 Recognizing Palindromes......................................... 120 3.6.2 A Simple Number Problem....................................... 121 3.6.3 A Simple Bank Account System................................. 122 3.6.4 Hamming's Problem .............................................. 125 3.6.5 Longest Ascending Subsequence ("Longest Up sequence") .. 127 3.6.6 Recognition and Parsing of Context-Free Grammars ......... 128 3.6.7 Reachability and Cycles in Graphs ............ ... .... ..... ... ... 129 3.6.8 A Coding Problem ................................................. 132 3.6.9 Unification of Terms ............................ '" .... ........... 134 3.6.10 The "Pack Problem" ............................................... 136 3.6.11 The Bounded Buffer .............................................. 138 3.6.12 Paraffins ............................................................ 139 3.7 Exercises ...................................................................... 142 4. Basic Transformation Techniques ......................................... 149 4.1 Semantic Foundations ....................................................... 149 4.2 Notational Conventions ..... ....... ........ ...... ......... ... .... ..... ... ... 154 4.2.1 Program Schemes ................................................. 154 4.2.2 Transformation Rules............................................. 156 4.2.3 Program Developments ........................................... 158 4.3 The UnfoldIFold System ................................................... 159 4.4 Further Basic Transformation Rules ............... ...... ....... ..... ... ... 163 4.4.1 Axiomatic Rules of the Language Definition ................... 164 4.4.2 Rules About Predicates ........................................... 166 4.4.3 Basic Set Theoretic Rules ........ ...... ... ...... ... ...... ... ...... 167 4.4.4 Rules from the Axioms of the Underlying Data Types ........ 168 4.4.5 Derived Basic Transformation Rules .......... ....... ..... ...... 168 4.5 Sample Developments with Basic Rules.................................. 178 4.5.1 Simple Number Problem ......................................... 178 4.5.2 Palindromes........................................................ 180 4.5.3 The Simple Bank Account Problem Continued................ 180 4.5.4 Floating Point Representation ofthe Dual Logarithm of the Factorial............. ......... ...... .... ........... .... ..... ... ...... 184 4.6 Exercises...................................................................... 185

Page 9

Conren~ Xl s. From Descriptive Specifications to Operational Ones .............. 189 5.1 Transfonning Specifications... . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 191 5.2 Embedding ................................................................ '" 195 5.3 Development of Recursive Solutions from Problem Descriptions .... 200 5.3.1 A General Strategy................................................. 200 5.3.2 Compact Rules for Particular Specification Constructs ....... 211 5.3.3 Compact Rules for Particular Data Types....................... 220 5.3.4 Developing Partial Functions from their Domain Restriction 225 5.4 Elimination of Descriptive Constructs in Applicative Programs.. ... ... 232 5.4.1 Use of Sets ......................................................... 233 5.4.2 Classical Backtracking ... ........... ......... ... ... .... ........... 236 5.4.3 Finite Look-Ahead................................................. 237 5.5 Examples ..................................................................... 239 5.5.1 Sorting.............................................................. 240 5.5.2 Recognition of Context-Free Grammars ........................ 241 5.5.3 Coding Problem ................................................... 247 5.5.4 Cycles in a Graph.................................................. 249 5.5.5 Hamming's Problem .............................................. 251 5.5.6 Unification of Terms .............................................. 252 5.5.7 The "Pack Problem" ............................................... 256 5.6 Exercises .. ..... ............... ................ ..... ............... ............ 259 6. Modification of AppIicative Programs................................... 263 6.1 Merging of Computations .................................................. 264 6.1.1 Function Composition ............................................ 264 6.1.2 Function Combination ............................................ 267 6.1.3 "Free Merging" ..................................................... 273 6.2 Inverting the Flow of Computation ....................................... 275 6.3 Storing of Values Instead of Recomputation ............................. 280 6.3.1 Memo-ization ....................................................... 280 6.3.2 Tabulation.......................................................... 282 6.4 Computation in Advance.................................................... 286 6.4.1 Relocation.......................................................... 287 6.4.2 Precomputation.................................................... 288 6.4.3 Partial Evaluation.................................................. 290 6.4.4 Differencing ........................................................ 292 6.5 Simplification of Recursion ................................................ 296 6.5.1 From Linear Recursion to Tail Recursion ...................... 297 6.5.2 From Non-Linear Recursion to Tail Recursion................ 303 6.5.3 From Systems of Recursive Functions to Single Recursive Functions ........................................................... 306 6.6 Examples ...................................................................... 310 6.6.1 Bottom-up Recognition of Context-Free Grammars .......... 310 6.6.2 The Algorithm by Cocke, Kasarni and Younger ............... 312 6.6.3 Cycles in a Graph .... ............... .............................. 316 6.6.4 Hamming's Problem .............................................. 319 6.7 Exercises........... .............. .......... ..... .... ............ ... ........... 322

Page 10

XII Contents 7. Transformation of Procedural Programs ............................... 326 7.1 From Tail Recursion to Iteration ........................................... 326 7.1.1 while Loops....................................................... 328 7.1.2 Jumps and Labels.................................................. 332 7.1.3 Further Loop Constructs .......................................... 335 7.2 Simplification of Imperative Programs.................................... 336 7.2.1 Sequentialization ................................................... 336 7.2.2 Elimination of Superfluous Assignments and Variables...... 337 7.2.3 Rearrangement of Statements..................................... 339 7.2.4 Procedures .......................................................... 341 7.3 Examples ..................................................................... 343 7.3.1 Hamming's Problem .............................................. 344 7.3.2 Cycles in a Graph.................................................. 345 7.4 Exercises. .... ...... ..... ...... ...... ...... ... ....... ..... .... ................. 347 8. Transformation of Data Structures ........................................ 349 8.1 Implementation of Types in Terms of Other Types ...................... 350 8.1.1 Theoretical Foundations .......................................... 351 8.1.2 Proving the Correctness of an Algebraic Implementation .... 355 8.2 Implementations of Types for Specific Environments .................. 359 8.2.1 Implementations by Computation Structures ................... 359 8.2.2 Implementations in Terms of Modes ............................ 361 8.2.3 Implementations in Terms of Pointers and Arrays....... ...... 370 8.2.3 Procedural Implementations...................................... 373 8.3 Libraries of Implementations ............................................... 375 8.3.1 "Ready-Made" Implementations ... ...... ......... .... ........ ... 376 8.3.2 Complexity and Efficiency.... ........... ...... ... ............... 379 8.4 Transformation of Type Systems .......................................... 381 8.5 Joint Development ........................................................... 386 8.5.1 Changing the Arguments of Functions ........ .... ..... .... ..... 387 8.5.2 "Attribution".. ...... ...... ...... ...... ...... .... ..... ... ...... ... ... 391 8.5.3 Compositions....................................................... 394 8.5.4 Transition to Procedural Constructs for Particular Data Types 395 8.6 An Example: Cycles in a Graph............................................ 398 8.7 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 401 9. Complete Examples ............................................................. 404 9.1 Warshall'sAlgorithm ....................................................... 405 9.1.1 Formal Problem Specification ................................... 405 9.1.2 Derivation of an Operational Specification..... .. ... .... .. ... ... 405 9.1. 3 Operational Improvements..... .. .... .. .... .. . .. .... .. . .. ... . ... .. 407 9.1.4 Transition to an Imperative Program ............................ 408 9.2 The Majority Problem ....................................................... 410 9.2.1 Formal Specification .............................................. 410 9.2.2 Development of an Algorithm for the Simple Problem ....... 411 9.2.3 Development of an Algorithm for the Generalized Problem .. 414

formal verification of programs and their transformations

2010 • 158 Pages • 996 KB

FORMAL VERIFICATION OF PROGRAMS AND THEIR TRANSFORMATIONS

2010 • 158 Pages • 996 KB

A Transformational Approach to Formal Digital System Design

2007 • 133 Pages • 780 KB

Specification of Model Transformation and Weaving in Model Driven Engineering

2007 • 132 Pages • 2.14 MB

Software Verification and Synthesis using Constraints and Program Transformation

2014 • 214 Pages • 1.21 MB

Model Transformation Approach to Automated Model Driven Development

2015 • 126 Pages • 1.1 MB

A query structured approach for model transformation

2014 • 90 Pages • 4.63 MB

Managing Software Requirements: A Use Case Approach

2003 • 521 Pages • 8.94 MB

Comparative Evaluation of Lighting Design Software Programs

2006 • 318 Pages • 9.17 MB

A Systemic Approach to Conflict Transformation

2008 • 101 Pages • 1.04 MB

A Semiotic Approach to Conflict Transformation

2017 • 170 Pages • 862 KB

A Biblical Approach to Social Transformation

2011 • 220 Pages • 945 KB

Transformation and Analysis of Functional Programs

2009 • 225 Pages • 702 KB

A Systemic Approach to Conflict Transformation. Exploring

2008 • 101 Pages • 1.04 MB

SOFTWARE DEVELOPMENT AND DOCUMENTATION

1995 • 76 Pages • 668 KB