Specification and transformation of programs : a formal approach to software development
著者
書誌事項
Specification and transformation of programs : a formal approach to software development
(Texts and monographs in computer science)
Springer-Verlag, c1990
- : gw
- : us : alk. paper
- : gw : soft : student ed
- : u.s. : soft : student ed
大学図書館所蔵 全29件
  青森
  岩手
  宮城
  秋田
  山形
  福島
  茨城
  栃木
  群馬
  埼玉
  千葉
  東京
  神奈川
  新潟
  富山
  石川
  福井
  山梨
  長野
  岐阜
  静岡
  愛知
  三重
  滋賀
  京都
  大阪
  兵庫
  奈良
  和歌山
  鳥取
  島根
  岡山
  広島
  山口
  徳島
  香川
  愛媛
  高知
  福岡
  佐賀
  長崎
  熊本
  大分
  宮崎
  鹿児島
  沖縄
  韓国
  中国
  タイ
  イギリス
  ドイツ
  スイス
  フランス
  ベルギー
  オランダ
  スウェーデン
  ノルウェー
  アメリカ
注記
Includes bibliographical reference(p.[456]-474) and index
内容説明・目次
内容説明
"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.
目次
1. Introduction.- 1.1 Software Engineering.- 1.2 The Problematics of Software Development.- 1.3 Formal Specification and Program Transformation.- 1.4 Our Particular View of Transformational Programming.- 1.5 Relation to Other Approaches to Programming Methodology.- 1.6 An Introductory Example.- 2. Requirements Engineering.- 2.1 Introduction.- 2.1.1 Basic Notions.- 2.1.2 Essential Criteria for Good Requirements Definitions.- 2.1.3 The Particular Role of Formality.- 2.2 Some Formalisms Used in Requirements Engineering.- 2.2.1 A Common Basis for Comparison.- 2.2.2 Flowcharts.- 2.2.3 Decision Tables.- 2.2.4 Formal Languages and Grammars.- 2.2.5 Finite State Mechanisms.- 2.2.6 Petri Nets.- 2.2.7 SA/SADT.- 2.2.8 PSL/PSA.- 2.2.9 RSL/REVS.- 2.2.10 EPOS.- 2.2.11 Gist.- 2.2.12 Summary.- 3. Formal Problem Specification.- 3.1 Specification and Formal Specification.- 3.2 The Process of Formalization.- 3.2.1 Problem Identification.- 3.2.2 Problem Description.- 3.2.3 Analysis of the Problem Description.- 3.3 Definition of Object Classes and Their Basic Operations.- 3.3.1 Algebraic Types.- 3.3.2 Further Examples of Basic Algebraic Types.- 3.3.3 Extensions of Basic Types.- 3.3.4 Formulation of Concepts as Algebraic Types.- 3.3.5 Modes.- 3.4 Additional Language Constructs for Formal Specifications.- 3.4.1 Applicative Language Constructs.- 3.4.2 Quantified Expressions.- 3.4.3 Choice and Description.- 3.4.4 Set Comprehension.- 3.4.5 Computation Structures.- 3.5 Structuring and Modularization.- 3.6 Examples.- 3.6.1 Recognizing Palindromes.- 3.6.2 A Simple Number Problem.- 3.6.3 A Simple Bank Account System.- 3.6.4 Hamming's Problem.- 3.6.5 Longest Ascending Subsequence ("Longest Upsequence").- 3.6.6 Recognition and Parsing of Context-Free Grammars.- 3.6.7 Reachability and Cycles in Graphs.- 3.6.8 A Coding Problem.- 3.6.9 Unification of Terms.- 3.6.10 The "Pack Problem".- 3.6.11 The Bounded Buffer.- 3.6.12 Paraffins.- 3.7 Exercises.- 4. Basic Transformation Techniques.- 4.1 Semantic Foundations.- 4.2 Notational Conventions.- 4.2.1 Program Schemes.- 4.2.2 Transformation Rules.- 4.2.3 Program Developments.- 4.3 The Unfold/Fold System.- 4.4 Further Basic Transformation Rules.- 4.4.1 Axiomatic Rules of the Language Definition.- 4.4.2 Rules About Predicates.- 4.4.3 Basic Set Theoretic Rules.- 4.4.4 Rules from the Axioms of the Underlying Data Types.- 4.4.5 Derived Basic Transformation Rules.- 4.5 Sample Developments with Basic Rules.- 4.5.1 Simple Number Problem.- 4.5.2 Palindromes.- 4.5.3 The Simple Bank Account Problem Continued.- 4.5.4 Floating Point Representation of. the Dual Logarithm of the Factorial.- 4.6 Exercises.- 5. From Descriptive Specifications to Operational Ones.- 5.1 Transforming Specifications.- 5.2 Embedding.- 5.3 Development of Recursive Solutions from Problem Descriptions.- 5.3.1 A General Strategy.- 5.3.2 Compact Rules for Particular Specification Constructs.- 5.3.3 Compact Rules for Particular Data Types.- 5.3.4 Developing Partial Functions from their Domain Restriction.- 5.4 Elimination of Descriptive Constructs in Applicative Programs.- 5.4.1 Use of Sets.- 5.4.2 Classical Backtracking.- 5.4.3 Finite Look-Ahead.- 5.5 Examples.- 5.5.1 Sorting.- 5.5.2 Recognition of Context-Free Grammars.- 5.5.3 Coding Problem.- 5.5.4 Cycles in a Graph.- 5.5.5 Hamming's Problem.- 5.5.6 Unification of Terms.- 5.5.7 The "Pack Problem".- 5.6 Exercises.- 6. Modification of Applicative Programs.- 6.1 Merging of Computations.- 6.1.1 Function Composition.- 6.1.2 Function Combination.- 6.1.3 "Free Merging".- 6.2 Inverting the Flow of Computation.- 6.3 Storing of Values Instead of Recomputation.- 6.3.1 Memo-ization.- 6.3.2 Tabulation.- 6.4 Computation in Advance.- 6.4.1 Relocation.- 6.4.2 Precomputation.- 6.4.3 Partial Evaluation.- 6.4.4 Differencing.- 6.5 Simplification of Recursion.- 6.5.1 From Linear Recursion to Tail Recursion.- 6.5.2 From Non-Linear Recursion to Tail Recursion.- 6.5.3 From Systems of Recursive Functions to Single Recursive Functions.- 6.6 Examples.- 6.6.1 Bottom-up Recognition of Context-Free Grammars.- 6.6.2 The Algorithm by Cocke, Kasami and Younger.- 6.6.3 Cycles in a Graph.- 6.6.4 Hamming's Problem.- 6.7 Exercises.- 7. Transformation of Procedural Programs.- 7.1 From Tail Recursion to Iteration.- 7.1.1 while Loops.- 7.1.2 Jumps and Labels.- 7.1.3 Further Loop Constructs.- 7.2 Simplification of Imperative Programs.- 7.2.1 Sequentialization.- 7.2.2 Elimination of Superfluous Assignments and Variables.- 7.2.3 Rearrangement of Statements.- 7.2.4 Procedures.- 7.3 Examples.- 7.3.1 Hamming's Problem.- 7.3.2 Cycles in a Graph.- 7.4 Exercises.- 8. Transformation of Data Structures.- 8.1 Implementation of Types in Terms of Other Types.- 8.1.1 Theoretical Foundations.- 8.1.2 Proving the Correctness of an Algebraic Implementation.- 8.2 Implementations of Types for Specific Environments.- 8.2.1 Implementations by Computation Structures.- 8.2.2 Implementations in Terms of Modes.- 8.2.3 Implementations in Terms of Pointers and Arrays.- 8.2.3 Procedural Implementations.- 8.3 Libraries of Implementations.- 8.3.1 "Ready-Made" Implementations.- 8.3.2 Complexity and Efficiency.- 8.4 Transformation of Type Systems.- 8.5 Joint Development.- 8.5.1 Changing the Arguments of Functions.- 8.5.2 "Attribution".- 8.5.3 Compositions.- 8.5.4 Transition to Procedural Constructs for Particular Data Types.- 8.6 An Example: Cycles in a Graph.- 8.7 Exercises.- 9. Complete Examples.- 9.1 Warshall's Algorithm.- 9.1.1 Formal Problem Specification.- 9.1.2 Derivation of an Operational Specification.- 9.1.3 Operational Improvements.- 9.1.4 Transition to an Imperative Program.- 9.2 The Majority Problem.- 9.2.1 Formal Specification.- 9.2.2 Development of an Algorithm for the Simple Problem.- 9.2.3 Development of an Algorithm for the Generalized Problem.- 9.3 Fast Pattern Matching According to Boyer and Moore.- 9.3.1 Formal Specification.- 9.3.2 Development of the Function occurs.- 9.3.3 Deriving an Operational Version of ?.- 9.3.4 Final Version of the Function occurs.- 9.3.5 Remarks on Further Development.- 9.3.6 Concluding Remarks.- 9.4 A Text Editor.- 9.4.1 Formal Specification.- 9.4.2 Transformational Development.- 9.4.3 Concluding Remarks.- References.
「Nielsen BookData」 より