В кінці книги назва українською мовою

Автори зазначені на обкладинці

Бібліографія: сторінки 297-311 (178 назв)

LIST OF ABBREVIATIONS AND NOTATIONS.....7
INTRODUCTION.....8
PART I. THEORETICAL BASIS OF FORMAL PROGRAM SPECIFICATION METHODS.....10
Chapter 1. Basic programming paradigms.....11
1.1. Imperative programming.....11
1.2. Functional and logic programming.....14
1.3. Theoretical programming.....17
1.3.1. Algebraic and insertion programming.....17
1.3.2. Algebra-algorithmic programming.....20
1.3.3. Composition-nominative programming.....24
1.3.3.1. Main principles of CNP.....25
1.3.3.2. Data structures in CNP.....28
1.3.3.3. Types of functions in CNP.....30
1.3.3.4. Compositions in CNP.....31
1.3.3.5. Program systems in CNP.....31
1.3.3.6. Applications of CNP.....32
1.4.Parallel programming.....32
1.4.1. Parallelism in computing systems....33
1.4.2. Parallel computing models.....35
1.5. Object-oriented and component-oriented programming.....46
Control questions.....50
Chapter 2. Algebras and specifications of algorithms.....51
2.1. Dijkstra algebra.....52
2.2. Algebra of flowgraphs.....58
2.3. Glushkov system of algorithmic algebras and its modifications.....62
2.4. Algebra of algorithmics.....70
Control questions and exercises.....75
Chapter 3. Algebraic programming based on rewriting rules.....77
3.1. Aspects of rewriting: definitions and examples.....77
3.1.1. Abstract rewriting systems.....77
3.1.2. Rewriting rules.....84
3.1.3. Rewriting of fragments...86
3.2. Term rewriting.....87
3.2.1. The alphabet of the system.....87
3.2.2. Terms.....87
3.2.3. Operations on terms.....88
3.2.4. Rewriting rules.....92
3.2.5. Rewriting strategy.....93
3.2.6. Interaction with an environment.....94
3.2.7. TermWare language.....96
3.3. Existing software implementations.....97
3.3.1. Maude.....97
3.3.2. Stratego.....98
3.3.3. ASF+SDF.....99
3.3.4. TXL.....101
3.3.5. Jess.....101
3.3.6. APS.....102
3.3.7. TermWare.....103
3.4. Applications of rewriting rules technique for working with program code.....103
3.4.1. The main directions of use.....103
3.4.2. The analysis of source code.....104
3.4.3. Refactoring.....107
3.4.4. Optimization.....108
3.4.5. Security.....109
3.4.6. Legacy code.....109
3.4.7. Domain-specific languages.....110
3.4.8. Extensions of languages.....111
3.4.9. Modelling.....112
Control questions and exercises.....113
Chapter 4. Generalization of Glushkov algorithmic algebra systems to the case of programs on hierarchical data.....116
4.1. Different types of nominative data.....116
4.2. Representation of data structures by nominative data.....120
4.3. Algebras of nominative data.....123
4.4. Operational semantics of operations on nominative data.....131
4.4.1. Terms and term rewriting systems.....133
4.4.2. Interpretation of terms and function symbols.....139
4.4.3. Term rewriting system representation of programs over complex-named data.....142
4.5. Compositions of functions and predicates over nominative data.....152
4.6. Generalized systems of Glushkov algorithmic algebras.....157
4.7. Stability and monotonicity of programs over nominative data.....158
Questions and exercises.....170
PART II. APPLICATION OF FORMAL PROGRAM SPECIFICATION METHODS FOR SOFTWARE DEVELOPMENT AND VERIFICATION.....171
Chapter 5. Formal design of algorithms and programs.....172
5.1. Metarules of algorithm specification design.....172
5.2. Algorithmic language SAA/1.....176
5.3. Algebra-grammatical models for generation of algorithm specifications.....180
5.3.1. Algebra of hyperschemes.....182
5.3.2. Application of hyperschemes to a representation of derivation algorithms in generative grammars.....186
5.4. Algebra-dynamic models of parallel programs.....193
5.4.1. The concept of a transition system.....194
5.4.2. Sequential program execution model.....195
5.4.3. Parallel program execution model.....199
5.4.4. Program transformations based on rewriting rules.....204
5.4.4.1. The transition from a sequential program to GPU program.....204
5.4.4.2. GPU program optimization.....205
5.4.4.3. The transition between high-level and low-level program models.....205
Control questions and exercises.....207
Chapter 6. Software tools for design and synthesis of programs.....211
6.1. The architecture of the integrated toolkit.....211
6.2. Dialogue design of algorithm schemes.....215
6.3. Generation of algorithms and programs.....224
6.3.1. Generation of regular schemes on the basis of hyperschemes.....225
6.3.2. Synthesis of programs on the basis of algorithm schemes.....227
6.4. The rewriting rules system.....237
6.4.1. The language of the TermWare system.....237
6.4.2. The structure of the rewriting rules toolkit.....239
6.4.3. Additional facilities of the rewriting rules toolkit .....241
Control questions and exercises.....248
Chapter 7. Automated development of efficient parallel programs.....250
7.1. Design and parallelization of programs for multicore processors.....250
7.2. Transformation of coordination-constructs in parallel programs.....257
7.3. Development of parallel programs for graphics processing units.....264
7.3.1. Parallel summation of elements of a numeric vector.....265
7.3.2. The Game of Life problem.....271
7.4. Formalization and verification of parallel programs using a proof assistant.....272
7.4.1. A simple parallel programming language.....272
7.4.2. Formalization of Peterson’s algorithm and the proof of the mutual exclusion property.....275
Exercises.....295
REFERENCES.....297
APPENDIX A. Models and source codes of examples.....312
A. 1. Finding the quantity of prime numbers.....312
A. 2. Simulation of one-dimensional Brownian motion.....314
A. 3. Parallel summation of elements of a numeric vector.....321
APPENDIX B. The text of the formal proof of a theorem in Mizar language.....324

Theoretical basis of formal specification of sequential and parallel programs based on algorithm algebra and rewriting rules technique is outlined. In the context of development of V. M. Glushkov’s ideas on formalization of programming languages, formal program specification methods are applied for solving software design and generation problems. Formalization and verification of programs are studied.
The book is for students of software engineering specialty, graduate students and teachers of computer training faculties of higher education institutions and also for specialists who develop applied algorithms and software in different areas.